diff --git a/Manual/Tools/polyscripter.sml b/Manual/Tools/polyscripter.sml
index 7b43875cb5..af93c1483d 100644
--- a/Manual/Tools/polyscripter.sml
+++ b/Manual/Tools/polyscripter.sml
@@ -17,11 +17,11 @@ fun lnumdie linenum extra exn =
 
 val outputPrompt = ref "> "
 
-val quote = QFRead.fromString
+val quote = HolParser.fromString
 val default_linewidth = 77
 
 fun quoteFile lnum fname =
-  QFRead.inputFile fname handle e => lnumdie lnum "" e
+  HolParser.inputFile fname handle e => lnumdie lnum "" e
 
 datatype lbuf =
          LB of {
@@ -319,7 +319,7 @@ fun process_line debugp umap obuf origline lbuf = let
     end
   val assertcmd = "##assert "
   val assertcmdsz = size assertcmd
-  val stringCReader = #read o QFRead.stringToReader true
+  val stringCReader = #read o HolParser.stringToReader true
   fun compile exnhandle input =
       (if debugp then
          TextIO.output(TextIO.stdErr, input)
diff --git a/developers/genUseScript.sml b/developers/genUseScript.sml
index 59db24f688..a9b3138cec 100644
--- a/developers/genUseScript.sml
+++ b/developers/genUseScript.sml
@@ -39,9 +39,9 @@ in
   (push, read, reset)
 end;
 
-val _ = use "../tools/Holmake/QuoteFilter.sml";
-val _ = use "../tools/Holmake/QFRead.sig";
-val _ = use "../tools/Holmake/QFRead.sml";
+val _ = use "../tools/Holmake/HolLex.sml";
+val _ = use "../tools/Holmake/HolParser.sig";
+val _ = use "../tools/Holmake/HolParser.sml";
 val _ = use "../tools/Holmake/Holdep_tokens.sig"
 val _ = use "../tools/Holmake/Holdep_tokens.sml";
 
diff --git a/src/AI/sml_inspection/smlExecute.sml b/src/AI/sml_inspection/smlExecute.sml
index e235aafcee..41788d20cf 100644
--- a/src/AI/sml_inspection/smlExecute.sml
+++ b/src/AI/sml_inspection/smlExecute.sml
@@ -29,7 +29,7 @@ val sml_thml_glob = ref []
 
 fun quse_string s =
   let
-    val stream = TextIO.openString (QFRead.fromString false s)
+    val stream = TextIO.openString (HolParser.fromString false s)
     fun infn () = TextIO.input1 stream
   in
     (
diff --git a/src/bool/boolScript.sml b/src/bool/boolScript.sml
index 35ab826ebf..09f5e3a950 100644
--- a/src/bool/boolScript.sml
+++ b/src/bool/boolScript.sml
@@ -68,11 +68,11 @@ fun mkloc(s,n) = DB_dtype.mkloc(s,n,true)
 fun def l (n,t) = Definition.located_new_definition {loc=mkloc l,name=n,def=t}
 fun thm l (n,th) = Theory.gen_save_thm{loc=mkloc l,name=n,private=false,thm=th}
 fun ax l (n,t) = Theory.gen_new_axiom(n,t,mkloc l)
-val T_DEF = def (#(FNAME),#(LINE))
+val T_DEF = def (#(FILE),#(LINE))
   ("T_DEF",
    “T = ((\x:bool. x) = \x:bool. x)”);
 
-val FORALL_DEF = def (#(FNAME), #(LINE))
+val FORALL_DEF = def (#(FILE), #(LINE))
     ("FORALL_DEF", “! = \P:'a->bool. P = \x. T”)
 
 val _ = set_fixity "!" Binder
@@ -80,7 +80,7 @@ val _ = unicode_version {u = UChar.forall, tmnm = "!"};
 val _ = TeX_notation {hol = "!", TeX = ("\\HOLTokenForall{}",1)}
 val _ = TeX_notation {hol = UChar.forall, TeX = ("\\HOLTokenForall{}",1)}
 
-val EXISTS_DEF = def (#(FNAME), #(LINE))
+val EXISTS_DEF = def (#(FILE), #(LINE))
                      ("EXISTS_DEF",     “? = \P:'a->bool. P ($@ P)”);
 
 val _ = set_fixity "?" Binder
@@ -88,7 +88,7 @@ val _ = unicode_version {u = UChar.exists, tmnm = "?"}
 val _ = TeX_notation {hol = "?", TeX = ("\\HOLTokenExists{}",1)}
 val _ = TeX_notation {hol = UChar.exists, TeX = ("\\HOLTokenExists{}",1)}
 
-val AND_DEF = def (#(FNAME), #(LINE))
+val AND_DEF = def (#(FILE), #(LINE))
             ("AND_DEF",        “/\ = \t1 t2. !t. (t1 ==> t2 ==> t) ==> t”);
 
 val _ = set_fixity "/\\" (Infixr 400);
@@ -97,7 +97,7 @@ val _ = TeX_notation {hol = "/\\", TeX = ("\\HOLTokenConj{}",1)}
 val _ = TeX_notation {hol = UChar.conj, TeX = ("\\HOLTokenConj{}",1)}
 
 
-val OR_DEF = def (#(FNAME), #(LINE))
+val OR_DEF = def (#(FILE), #(LINE))
    ("OR_DEF",         “\/ = \t1 t2. !t. (t1 ==> t) ==> (t2 ==> t) ==> t”)
 
 val _ = set_fixity "\\/" (Infixr 300)
@@ -106,10 +106,10 @@ val _ = TeX_notation {hol = "\\/", TeX = ("\\HOLTokenDisj{}",1)}
 val _ = TeX_notation {hol = UChar.disj, TeX = ("\\HOLTokenDisj{}",1)}
 
 
-val F_DEF = def (#(FNAME), #(LINE))
+val F_DEF = def (#(FILE), #(LINE))
    ("F_DEF",          “F = !t. t”);
 
-val NOT_DEF = def (#(FNAME), #(LINE))
+val NOT_DEF = def (#(FILE), #(LINE))
    ("NOT_DEF",        “~ = \t. t ==> F”);
 
 (* now allows parsing of not equal *)
@@ -123,7 +123,7 @@ val _ = TeX_notation {hol=UChar.neq, TeX = ("\\HOLTokenNotEqual{}",1)}
 
 
 
-val EXISTS_UNIQUE_DEF = def (#(FNAME), #(LINE))
+val EXISTS_UNIQUE_DEF = def (#(FILE), #(LINE))
   ("EXISTS_UNIQUE_DEF",
    “?! = \P:'a->bool. $? P /\ !x y. P x /\ P y ==> (x=y)”);
 
@@ -133,23 +133,23 @@ val _ = unicode_version { u = UChar.exists ^ "!", tmnm = "?!"}
 val _ = TeX_notation {hol = "?!", TeX = ("\\HOLTokenUnique{}",2)}
 val _ = TeX_notation {hol = UChar.exists ^ "!", TeX = ("\\HOLTokenUnique{}",2)}
 
-val LET_DEF = def (#(FNAME), #(LINE))
+val LET_DEF = def (#(FILE), #(LINE))
    ("LET_DEF",        “LET = λ(f:'a->'b) x. f x”);
 
-val COND_DEF = def (#(FNAME), #(LINE))
+val COND_DEF = def (#(FILE), #(LINE))
    ("COND_DEF",       “COND = \t t1 t2.
                                       @x:'a. ((t=T) ==> (x=t1)) /\
                                              ((t=F) ==> (x=t2))”);
 val _ = overload_on ("case", “COND”)
 
-val ONE_ONE_DEF = def (#(FNAME), #(LINE))
+val ONE_ONE_DEF = def (#(FILE), #(LINE))
    ("ONE_ONE_DEF",    “ONE_ONE = \f:'a->'b. !x1 x2.
                                          (f x1 = f x2) ==> (x1 = x2)”);
 
-val ONTO_DEF = def (#(FNAME), #(LINE))
+val ONTO_DEF = def (#(FILE), #(LINE))
    ("ONTO_DEF",       “ONTO = \f:'a->'b. !y. ?x. y = f x”);
 
-val TYPE_DEFINITION = def (#(FNAME), #(LINE))
+val TYPE_DEFINITION = def (#(FILE), #(LINE))
    ("TYPE_DEFINITION",
                       “TYPE_DEFINITION = \P:'a->bool. \rep:'b->'a.
                               (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\
@@ -216,16 +216,16 @@ val _ = add_rule{term_name   = "COND",
  * HOL logic was provable.                                                   *
  *---------------------------------------------------------------------------*)
 
-val BOOL_CASES_AX = ax(#(FNAME), #(LINE))
+val BOOL_CASES_AX = ax(#(FILE), #(LINE))
    ("BOOL_CASES_AX", “!t. (t=T) \/ (t=F)”);
 
-val ETA_AX = ax(#(FNAME), #(LINE))
+val ETA_AX = ax(#(FILE), #(LINE))
    ("ETA_AX",        “!t:'a->'b. (\x. t x) = t”);
 
-val SELECT_AX = ax(#(FNAME), #(LINE))
+val SELECT_AX = ax(#(FILE), #(LINE))
    ("SELECT_AX",     “!(P:'a->bool) x. P x ==> P ($@ P)”);
 
-val INFINITY_AX = ax(#(FNAME), #(LINE))
+val INFINITY_AX = ax(#(FILE), #(LINE))
    ("INFINITY_AX",   “?f:ind->ind. ONE_ONE f /\ ~ONTO f”);
 
 
@@ -235,12 +235,12 @@ val INFINITY_AX = ax(#(FNAME), #(LINE))
 
 val arb = new_constant("ARB",alpha);  (* Doesn't have to be defined at all. *)
 
-val literal_case_DEF = def (#(FNAME), #(LINE))
+val literal_case_DEF = def (#(FILE), #(LINE))
    ("literal_case_DEF",  “literal_case = λ(f:'a->'b) x. f x”);
 
 val _ = overload_on ("case", “bool$literal_case”);
 
-val IN_DEF = def (#(FNAME), #(LINE))
+val IN_DEF = def (#(FILE), #(LINE))
    ("IN_DEF",         “IN = \x (f:'a->bool). f x”);
 
 val _ = set_fixity "IN" (Infix(NONASSOC, 425))
@@ -248,24 +248,24 @@ val _ = unicode_version {u = UChar.setelementof, tmnm = "IN"};
 val _ = TeX_notation {hol = "IN", TeX = ("\\HOLTokenIn{}",1)}
 val _ = TeX_notation {hol = UChar.setelementof, TeX = ("\\HOLTokenIn{}",1)}
 
-val RES_FORALL_DEF = def (#(FNAME), #(LINE))
+val RES_FORALL_DEF = def (#(FILE), #(LINE))
    ("RES_FORALL_DEF", “RES_FORALL = \p m. !x : 'a. x IN p ==> m x”);
 
 val _ = associate_restriction ("!",  "RES_FORALL")
 
-val RES_EXISTS_DEF = def (#(FNAME), #(LINE))
+val RES_EXISTS_DEF = def (#(FILE), #(LINE))
    ("RES_EXISTS_DEF", “RES_EXISTS = \p m. ?x : 'a. x IN p /\ m x”);
 
 val _ = associate_restriction ("?",  "RES_EXISTS")
 
-val RES_EXISTS_UNIQUE_DEF = def (#(FNAME), #(LINE))
+val RES_EXISTS_UNIQUE_DEF = def (#(FILE), #(LINE))
    ("RES_EXISTS_UNIQUE_DEF",
     “RES_EXISTS_UNIQUE =
           \p m. (?(x : 'a) :: p. m x) /\ !x y :: p. m x /\ m y ==> (x = y)”);
 
 val _ = associate_restriction ("?!",  "RES_EXISTS_UNIQUE");
 
-val RES_SELECT_DEF = def (#(FNAME), #(LINE))
+val RES_SELECT_DEF = def (#(FILE), #(LINE))
    ("RES_SELECT_DEF", “RES_SELECT = \p m. @x : 'a. x IN p /\ m x”);
 
 val _ = associate_restriction ("@",  "RES_SELECT")
@@ -276,7 +276,7 @@ val _ = associate_restriction ("@",  "RES_SELECT")
 (* Experimental rewriting directives                                         *)
 (*---------------------------------------------------------------------------*)
 
-val BOUNDED_DEF = def (#(FNAME), #(LINE))
+val BOUNDED_DEF = def (#(FILE), #(LINE))
     ("BOUNDED_DEF",
      “BOUNDED = λ(v:bool). T”);
 
@@ -284,7 +284,7 @@ val BOUNDED_DEF = def (#(FNAME), #(LINE))
 (* Support for detecting datatypes in theory files                           *)
 (*---------------------------------------------------------------------------*)
 
-val DATATYPE_TAG_DEF = def (#(FNAME), #(LINE))
+val DATATYPE_TAG_DEF = def (#(FILE), #(LINE))
     ("DATATYPE_TAG_DEF",
      “DATATYPE = \x. T”);
 
@@ -421,7 +421,7 @@ val ya = Av "y"
  *  |- T
  *---------------------------------------------------------------------------*)
 
-val TRUTH = thm (#(FNAME),#(LINE))
+val TRUTH = thm (#(FILE),#(LINE))
   ("TRUTH", EQ_MP (SYM T_DEF) (REFL “\x:bool. x”));
 
 fun EQT_ELIM th = EQ_MP (SYM th) TRUTH;
@@ -460,7 +460,7 @@ infixr ==>
 val op==> = mk_imp
 infix ==
 val op== = mk_eq
-val IMP_ANTISYM_AX = thm (#(FNAME), #(LINE))(
+val IMP_ANTISYM_AX = thm (#(FILE), #(LINE))(
   "IMP_ANTISYM_AX",
   let fun dsch t1 t2 th = DISCH (t2 ==> t1) (DISCH (t1 ==> t2) th)
       fun sch t1 t2 = (t1==>t2) ==> (t2==>t1) ==> (t1 == t2)
@@ -484,7 +484,7 @@ fun IMP_ANTISYM_RULE th1 th2 =
  * |- !t. F ==> t
  *---------------------------------------------------------------------------*)
 
-val FALSITY = thm (#(FNAME), #(LINE))("FALSITY", GEN tb (FALSITY_CONV tb))
+val FALSITY = thm (#(FILE), #(LINE))("FALSITY", GEN tb (FALSITY_CONV tb))
 
 fun CONTR tm th = MP (SPEC tm FALSITY) th
 
@@ -592,14 +592,14 @@ fun SELECT_RULE th =
      ETA_THM = |- !M. (\x. M x) = M
  ---------------------------------------------------------------------------*)
 
-val ETA_THM = thm (#(FNAME), #(LINE))
+val ETA_THM = thm (#(FILE), #(LINE))
                   ("ETA_THM", GEN_ALL(ETA_CONV “\x:'a. (M x:'b)”));
 
 (*---------------------------------------------------------------------------
  *  |- !t. t \/ ~t
  *---------------------------------------------------------------------------*)
 
-val EXCLUDED_MIDDLE = thm (#(FNAME), #(LINE))(
+val EXCLUDED_MIDDLE = thm (#(FILE), #(LINE))(
   "EXCLUDED_MIDDLE",
   let val th1 = RIGHT_BETA(AP_THM NOT_DEF tb)
       val th2 = DISJ1 (EQT_ELIM (ASSUME (tb == T))) (mk_neg tb)
@@ -623,7 +623,7 @@ fun IMP_ELIM th =
  *  |- !f y. (\x. f x) y = f y                                               *
  *---------------------------------------------------------------------------*)
 
-val BETA_THM = thm (#(FNAME), #(LINE))(
+val BETA_THM = thm (#(FILE), #(LINE))(
   "BETA_THM",
   GENL [fabt, ya] (BETA_CONV “(\x. (f:'a->'b) x) y”))
 
@@ -631,19 +631,19 @@ val BETA_THM = thm (#(FNAME), #(LINE))(
      LET_THM = |- !f x. LET f x = f x
  ---------------------------------------------------------------------------*)
 
-val LET_THM = thm (#(FNAME), #(LINE))(
+val LET_THM = thm (#(FILE), #(LINE))(
   "LET_THM",
   GEN fabt (GEN xa
     (RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM LET_DEF fabt)) xa))))
 
 (* |- $! f <=> !x. f x *)
-val FORALL_THM = thm (#(FNAME), #(LINE))(
+val FORALL_THM = thm (#(FILE), #(LINE))(
   "FORALL_THM",
   SYM (AP_TERM “$! :('a->bool)->bool”
                (ETA_CONV “\x:'a. f x:bool”)))
 
 (* |- $? f <=> ?x. f x *)
-val EXISTS_THM = thm (#(FNAME), #(LINE))(
+val EXISTS_THM = thm (#(FILE), #(LINE))(
   "EXISTS_THM",
   SYM (AP_TERM “$? :('a->bool)->bool”
                (ETA_CONV “\x:'a. f x:bool”)));
@@ -652,7 +652,7 @@ val EXISTS_THM = thm (#(FNAME), #(LINE))(
  *  |- !t1:'a. !t2:'b. (\x. t1) t2 = t1                                      *
  *---------------------------------------------------------------------------*)
 
-val ABS_SIMP = thm (#(FNAME), #(LINE))("ABS_SIMP",
+val ABS_SIMP = thm (#(FILE), #(LINE))("ABS_SIMP",
    GENL [“t1:'a”, “t2:'b”]
         (BETA_CONV “(\x:'b. t1:'a) t2”));
 
@@ -660,7 +660,7 @@ val ABS_SIMP = thm (#(FNAME), #(LINE))("ABS_SIMP",
  *   |- !t. (!x.t)  =  t
  *---------------------------------------------------------------------------*)
 
-val FORALL_SIMP = thm (#(FNAME), #(LINE))(
+val FORALL_SIMP = thm (#(FILE), #(LINE))(
   "FORALL_SIMP",
   GEN tb (IMP_ANTISYM_RULE
            (DISCH “!^xa. ^tb” (SPEC xa (ASSUME “!^xa.^tb”)))
@@ -670,7 +670,7 @@ val FORALL_SIMP = thm (#(FNAME), #(LINE))(
  *   |- !t. (?x.t)  =  t
  *---------------------------------------------------------------------------*)
 
-val EXISTS_SIMP = thm (#(FNAME), #(LINE))(
+val EXISTS_SIMP = thm (#(FILE), #(LINE))(
   "EXISTS_SIMP",
   let val ext = mk_exists(xa,tb)
   in
@@ -683,7 +683,7 @@ val EXISTS_SIMP = thm (#(FNAME), #(LINE))(
  *       |- !t1 t2. t1 ==> t2 ==> t1 /\ t2
  *---------------------------------------------------------------------------*)
 
-val AND_INTRO_THM = thm (#(FNAME), #(LINE))(
+val AND_INTRO_THM = thm (#(FILE), #(LINE))(
   "AND_INTRO_THM",
    let val t12 = t1b ==> t2b ==> tb
        val th1 = GEN tb (DISCH t12 (MP (MP (ASSUME t12)
@@ -698,7 +698,7 @@ val AND_INTRO_THM = thm (#(FNAME), #(LINE))(
  * |- !t1 t2. t1 /\ t2 ==> t1
  *---------------------------------------------------------------------------*)
 
-val AND1_THM = thm (#(FNAME), #(LINE))(
+val AND1_THM = thm (#(FILE), #(LINE))(
   "AND1_THM",
   let val t12 = mk_conj(t1b, t2b)
       val th2 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM AND_DEF t1b)) t2b)
@@ -712,7 +712,7 @@ val AND1_THM = thm (#(FNAME), #(LINE))(
  *    |- !t1 t2. t1 /\ t2 ==> t2
  *---------------------------------------------------------------------------*)
 
-val AND2_THM = thm (#(FNAME), #(LINE))("AND2_THM",
+val AND2_THM = thm (#(FILE), #(LINE))("AND2_THM",
   let val t1 = “t1:bool”
       and t2 = “t2:bool”
       val th1 = ASSUME “^t1 /\ ^t2”
@@ -736,7 +736,7 @@ val LIST_CONJ = end_itlist CONJ
  *   |- !t1 t2. (t1 /\ t2) = (t2 /\ t1)
  *---------------------------------------------------------------------------*)
 
-val CONJ_SYM = thm (#(FNAME), #(LINE))("CONJ_SYM",
+val CONJ_SYM = thm (#(FILE), #(LINE))("CONJ_SYM",
   let val t1 = “t1:bool”
       and t2 = “t2:bool”
       val th1 = ASSUME “^t1 /\ ^t2”
@@ -749,13 +749,13 @@ val CONJ_SYM = thm (#(FNAME), #(LINE))("CONJ_SYM",
                         (CONJ(CONJUNCT2 th2)(CONJUNCT1 th2)))))
   end);
 
-val _ = thm (#(FNAME), #(LINE))("CONJ_COMM", CONJ_SYM);
+val _ = thm (#(FILE), #(LINE))("CONJ_COMM", CONJ_SYM);
 
 (*---------------------------------------------------------------------------
  * |- !t1 t2 t3. t1 /\ (t2 /\ t3) = (t1 /\ t2) /\ t3
  *---------------------------------------------------------------------------*)
 
-val CONJ_ASSOC = thm (#(FNAME), #(LINE))("CONJ_ASSOC",
+val CONJ_ASSOC = thm (#(FILE), #(LINE))("CONJ_ASSOC",
   let val t1 = “t1:bool”
       and t2 = “t2:bool”
       and t3 = “t3:bool”
@@ -777,7 +777,7 @@ val CONJ_ASSOC = thm (#(FNAME), #(LINE))("CONJ_ASSOC",
  *  |- !t1 t2. t1 ==> t1 \/ t2
  *---------------------------------------------------------------------------*)
 
-val OR_INTRO_THM1 = thm (#(FNAME), #(LINE))("OR_INTRO_THM1",
+val OR_INTRO_THM1 = thm (#(FILE), #(LINE))("OR_INTRO_THM1",
   let val t = “t:bool”
       and t1 = “t1:bool”
       and t2 = “t2:bool”
@@ -793,7 +793,7 @@ val OR_INTRO_THM1 = thm (#(FNAME), #(LINE))("OR_INTRO_THM1",
  * |- !t1 t2. t2 ==> t1 \/ t2
  *---------------------------------------------------------------------------*)
 
-val OR_INTRO_THM2 = thm (#(FNAME), #(LINE))("OR_INTRO_THM2",
+val OR_INTRO_THM2 = thm (#(FILE), #(LINE))("OR_INTRO_THM2",
   let val t  = “t:bool”
       and t1 = “t1:bool”
       and t2 = “t2:bool”
@@ -809,7 +809,7 @@ val OR_INTRO_THM2 = thm (#(FNAME), #(LINE))("OR_INTRO_THM2",
  * |- !t t1 t2. (t1 \/ t2) ==> (t1 ==> t) ==> (t2 ==> t) ==> t
  *---------------------------------------------------------------------------*)
 
-val OR_ELIM_THM = thm (#(FNAME), #(LINE))("OR_ELIM_THM",
+val OR_ELIM_THM = thm (#(FILE), #(LINE))("OR_ELIM_THM",
    let val t =  “t:bool”
        and t1 = “t1:bool”
        and t2 = “t2:bool”
@@ -832,7 +832,7 @@ fun DISJ_CASES_UNION dth ath bth =
  * |- !t. (t ==> F) ==> ~t
  *---------------------------------------------------------------------------*)
 
-val IMP_F = thm (#(FNAME), #(LINE))("IMP_F",
+val IMP_F = thm (#(FILE), #(LINE))("IMP_F",
    let val t = “t:bool”
        val th1 = RIGHT_BETA (AP_THM NOT_DEF t)
    in
@@ -844,7 +844,7 @@ val IMP_F = thm (#(FNAME), #(LINE))("IMP_F",
  * |- !t. ~t ==> (t ==> F)
  *---------------------------------------------------------------------------*)
 
-val F_IMP = thm (#(FNAME), #(LINE))("F_IMP",
+val F_IMP = thm (#(FILE), #(LINE))("F_IMP",
    let val t = “t:bool”
        val th1 = RIGHT_BETA(AP_THM NOT_DEF t)
    in
@@ -856,7 +856,7 @@ val F_IMP = thm (#(FNAME), #(LINE))("F_IMP",
  * |- !t. ~t ==> (t=F)
  *---------------------------------------------------------------------------*)
 
-val NOT_F = thm (#(FNAME), #(LINE))("NOT_F",
+val NOT_F = thm (#(FILE), #(LINE))("NOT_F",
    let val t = “t:bool”
        val th1 = MP (SPEC t F_IMP) (ASSUME “~ ^t”)
        and th2 = SPEC t FALSITY
@@ -869,7 +869,7 @@ val NOT_F = thm (#(FNAME), #(LINE))("NOT_F",
  *  |- !t. ~(t /\ ~t)
  *---------------------------------------------------------------------------*)
 
-val NOT_AND = thm (#(FNAME), #(LINE))("NOT_AND",
+val NOT_AND = thm (#(FILE), #(LINE))("NOT_AND",
    let val th = ASSUME “t /\ ~t”
    in NOT_INTRO(DISCH “t /\ ~t” (MP (CONJUNCT2 th) (CONJUNCT1 th)))
    end);
@@ -944,7 +944,7 @@ val AND_CLAUSE5 =
  *         (t /\ t) = t
  *---------------------------------------------------------------------------*)
 
-val AND_CLAUSES = thm (#(FNAME), #(LINE))("AND_CLAUSES",
+val AND_CLAUSES = thm (#(FILE), #(LINE))("AND_CLAUSES",
    let val t = “t:bool”
    in
    GEN t (LIST_CONJ [SPEC t AND_CLAUSE1, SPEC t AND_CLAUSE2,
@@ -1025,7 +1025,7 @@ val OR_CLAUSE5 =
  *        (t \/ t) = t
  *---------------------------------------------------------------------------*)
 
-val OR_CLAUSES = thm (#(FNAME), #(LINE))("OR_CLAUSES",
+val OR_CLAUSES = thm (#(FILE), #(LINE))("OR_CLAUSES",
    let val t = “t:bool”
    in
    GEN t (LIST_CONJ [SPEC t OR_CLAUSE1, SPEC t OR_CLAUSE2,
@@ -1094,7 +1094,7 @@ val IMP_CLAUSE5 =
  *         (t ==> F) = ~t
  *---------------------------------------------------------------------------*)
 
-val IMP_CLAUSES = thm (#(FNAME), #(LINE))("IMP_CLAUSES",
+val IMP_CLAUSES = thm (#(FILE), #(LINE))("IMP_CLAUSES",
    let val t = “t:bool”
    in GEN t
       (LIST_CONJ [SPEC t IMP_CLAUSE1, SPEC t IMP_CLAUSE3,
@@ -1114,7 +1114,7 @@ val EQ_IMPLIES =
     val th0 = MK_COMB(impt1,t1_eq_t2)
     val imp_refl = IMP_CLAUSES |> SPEC t1b |> CONJUNCTS |> el 4 |> EQT_ELIM
   in
-    thm (#(FNAME), #(LINE))(
+    thm (#(FILE), #(LINE))(
       "EQ_IMPLIES", EQ_MP th0 imp_refl |> DISCH eqt |> GENL [t1b,t2b]
     )
   end
@@ -1124,7 +1124,7 @@ val EQ_IMPLIES =
  *    |- (~~t = t) /\ (~T = F) /\ (~F = T)
  *---------------------------------------------------------------------------*)
 
-val NOT_CLAUSES = thm (#(FNAME), #(LINE))("NOT_CLAUSES",
+val NOT_CLAUSES = thm (#(FILE), #(LINE))("NOT_CLAUSES",
  CONJ
   (GEN “t:bool”
     (IMP_ANTISYM_RULE
@@ -1143,20 +1143,20 @@ val NOT_CLAUSES = thm (#(FNAME), #(LINE))("NOT_CLAUSES",
  *   |- !x. x=x
  *---------------------------------------------------------------------------*)
 
-val EQ_REFL = thm (#(FNAME), #(LINE))("EQ_REFL", GEN “x : 'a” (REFL “x : 'a”));
+val EQ_REFL = thm (#(FILE), #(LINE))("EQ_REFL", GEN “x : 'a” (REFL “x : 'a”));
 
 (*---------------------------------------------------------------------------
  *   |- !x. (x=x) = T
  *---------------------------------------------------------------------------*)
 
-val REFL_CLAUSE = thm (#(FNAME), #(LINE))("REFL_CLAUSE",
+val REFL_CLAUSE = thm (#(FILE), #(LINE))("REFL_CLAUSE",
   GEN “x: 'a” (EQT_INTRO(SPEC “x:'a” EQ_REFL)));
 
 (*---------------------------------------------------------------------------
  *   |- !x y. x=y  ==>  y=x
  *---------------------------------------------------------------------------*)
 
-val EQ_SYM = thm (#(FNAME), #(LINE))("EQ_SYM",
+val EQ_SYM = thm (#(FILE), #(LINE))("EQ_SYM",
  let val x = “x:'a”
      and y = “y:'a”
  in
@@ -1167,7 +1167,7 @@ val EQ_SYM = thm (#(FNAME), #(LINE))("EQ_SYM",
  *    |- !x y. (x = y) = (y = x)
  *---------------------------------------------------------------------------*)
 
-val EQ_SYM_EQ = thm (#(FNAME), #(LINE))("EQ_SYM_EQ",
+val EQ_SYM_EQ = thm (#(FILE), #(LINE))("EQ_SYM_EQ",
    GEN “x:'a”
     (GEN “y:'a”
       (IMP_ANTISYM_RULE (SPEC “y:'a” (SPEC “x:'a” EQ_SYM))
@@ -1177,7 +1177,7 @@ val EQ_SYM_EQ = thm (#(FNAME), #(LINE))("EQ_SYM_EQ",
  *    |- !f g. (!x. f x = g x)  ==>  f=g
  *---------------------------------------------------------------------------*)
 
-val EQ_EXT = thm (#(FNAME), #(LINE))("EQ_EXT",
+val EQ_EXT = thm (#(FILE), #(LINE))("EQ_EXT",
    let val f = “f:'a->'b”
        and g = “g: 'a -> 'b”
    in
@@ -1189,7 +1189,7 @@ val EQ_EXT = thm (#(FNAME), #(LINE))("EQ_EXT",
       FUN_EQ_THM  |- !f g. (f = g) = !x. f x = g x
  ---------------------------------------------------------------------------*)
 
-val FUN_EQ_THM = thm (#(FNAME), #(LINE))("FUN_EQ_THM",
+val FUN_EQ_THM = thm (#(FILE), #(LINE))("FUN_EQ_THM",
   let val f = mk_var("f", Type.alpha --> Type.beta)
       val g = mk_var("g", Type.alpha --> Type.beta)
       val x = mk_var("x", Type.alpha)
@@ -1207,7 +1207,7 @@ val FUN_EQ_THM = thm (#(FNAME), #(LINE))("FUN_EQ_THM",
  *    |- !x y z. x=y  /\  y=z  ==>  x=z
  *---------------------------------------------------------------------------*)
 
-val EQ_TRANS = thm (#(FNAME), #(LINE))("EQ_TRANS",
+val EQ_TRANS = thm (#(FILE), #(LINE))("EQ_TRANS",
    let val x = “x:'a”
        and y = “y:'a”
        and z = “z:'a”
@@ -1225,7 +1225,7 @@ val EQ_TRANS = thm (#(FNAME), #(LINE))("EQ_TRANS",
  *     |- ~(T=F) /\ ~(F=T)
  *---------------------------------------------------------------------------*)
 
-val BOOL_EQ_DISTINCT = thm (#(FNAME), #(LINE))("BOOL_EQ_DISTINCT",
+val BOOL_EQ_DISTINCT = thm (#(FILE), #(LINE))("BOOL_EQ_DISTINCT",
    let val TF = “T = F”
        and FT = “F = T”
    in
@@ -1299,7 +1299,7 @@ val EQ_CLAUSE4 =
  *          (t = F)  =  ~t
  *---------------------------------------------------------------------------*)
 
-val EQ_CLAUSES = thm (#(FNAME), #(LINE))("EQ_CLAUSES",
+val EQ_CLAUSES = thm (#(FILE), #(LINE))("EQ_CLAUSES",
    let val t = “t:bool”
    in
    GEN t (LIST_CONJ [SPEC t EQ_CLAUSE1, SPEC t EQ_CLAUSE2,
@@ -1378,7 +1378,7 @@ val COND_CLAUSE2 =
  *    |- !t1:'a.!t2:'a. ((T => t1 | t2) = t1) /\ ((F => t1 | t2) = t2)
  *---------------------------------------------------------------------------*)
 
-val COND_CLAUSES = thm (#(FNAME), #(LINE))("COND_CLAUSES",
+val COND_CLAUSES = thm (#(FILE), #(LINE))("COND_CLAUSES",
    let val (t1,t2) = (“t1:'a”, “t2:'a”)
    in
    GEN t1 (GEN t2 (CONJ(SPEC t2(SPEC t1 COND_CLAUSE1))
@@ -1390,7 +1390,7 @@ val COND_CLAUSES = thm (#(FNAME), #(LINE))("COND_CLAUSES",
 (*                                                         TFM 90.07.23 *)
 (*--------------------------------------------------------------------- *)
 
-val COND_ID = thm (#(FNAME), #(LINE))("COND_ID",
+val COND_ID = thm (#(FILE), #(LINE))("COND_ID",
    let val b = “b:bool”
        and t = “t:'a”
        val def = INST_TYPE [beta |-> alpha] COND_DEF
@@ -1422,7 +1422,7 @@ val COND_ID = thm (#(FNAME), #(LINE))("COND_ID",
       SELECT_THM = |- !P. P (@x. P x) = ?x. P x
  ---------------------------------------------------------------------------*)
 
-val SELECT_THM = thm (#(FNAME), #(LINE))("SELECT_THM",
+val SELECT_THM = thm (#(FILE), #(LINE))("SELECT_THM",
   GEN “P:'a->bool”
    (SYM (RIGHT_BETA(RIGHT_BETA
           (AP_THM EXISTS_DEF “\x:'a. P x:bool”)))));
@@ -1431,7 +1431,7 @@ val SELECT_THM = thm (#(FNAME), #(LINE))("SELECT_THM",
 (* SELECT_REFL = |- !x. (@y. y = x) = x                                 *)
 (* ---------------------------------------------------------------------*)
 
-val SELECT_REFL = thm (#(FNAME), #(LINE))("SELECT_REFL",
+val SELECT_REFL = thm (#(FILE), #(LINE))("SELECT_REFL",
   let val th1 = SPEC “x:'a” (SPEC “\y:'a. y = x” SELECT_AX)
       val ths = map BETA_CONV [“(\y:'a. y = x) x”,
                                “(\y:'a. y = x)(@y. y = x)”]
@@ -1441,7 +1441,7 @@ val SELECT_REFL = thm (#(FNAME), #(LINE))("SELECT_REFL",
   GEN “x:'a” (MP th2 (REFL “x:'a”))
   end);
 
-val SELECT_REFL_2 = thm (#(FNAME), #(LINE))("SELECT_REFL_2",
+val SELECT_REFL_2 = thm (#(FILE), #(LINE))("SELECT_REFL_2",
   let val x = mk_var("x",   Type.alpha)
       val y = mk_var("y",   Type.alpha)
       val th1 = REFL x
@@ -1458,7 +1458,7 @@ val SELECT_REFL_2 = thm (#(FNAME), #(LINE))("SELECT_REFL_2",
 (* SELECT_UNIQUE = |- !P x. (!y. P y = (y = x)) ==> ($@ P = x)               *)
 (*---------------------------------------------------------------------------*)
 
-val SELECT_UNIQUE = thm (#(FNAME), #(LINE))("SELECT_UNIQUE",
+val SELECT_UNIQUE = thm (#(FILE), #(LINE))("SELECT_UNIQUE",
   let fun mksym tm = DISCH tm (SYM(ASSUME tm))
       val th0 = IMP_ANTISYM_RULE (mksym “y:'a = x”)
                                  (mksym “x:'a = y”)
@@ -1495,7 +1495,7 @@ val SELECT_ELIM_THM = let
   val PselP_th0 = UNDISCH (SPEC_ALL SELECT_AX)
   val PselP_th = CHOOSE(x, ex_th) PselP_th0
 in
-  thm (#(FNAME), #(LINE))(
+  thm (#(FILE), #(LINE))(
     "SELECT_ELIM_THM",
     GENL [P, Q] (DISCH_ALL (MP imp_th PselP_th))
   )
@@ -1505,7 +1505,7 @@ end
 (* NOT_FORALL_THM = |- !P. ~(!x. P x) = ?x. ~P x                            *)
 (* -------------------------------------------------------------------------*)
 
-val NOT_FORALL_THM = thm (#(FNAME), #(LINE))("NOT_FORALL_THM",
+val NOT_FORALL_THM = thm (#(FILE), #(LINE))("NOT_FORALL_THM",
     let val f = “P:'a->bool”
         val x = “x:'a”
         val t = mk_comb(f,x)
@@ -1525,7 +1525,7 @@ val NOT_FORALL_THM = thm (#(FNAME), #(LINE))("NOT_FORALL_THM",
 (* NOT_EXISTS_THM = |- !P. ~(?x. P x) = (!x. ~P x)                          *)
 (* ------------------------------------------------------------------------- *)
 
-val NOT_EXISTS_THM = thm (#(FNAME), #(LINE))("NOT_EXISTS_THM",
+val NOT_EXISTS_THM = thm (#(FILE), #(LINE))("NOT_EXISTS_THM",
     let val f = “P:'a->bool”
         val x = “x:'a”
         val t = mk_comb(f,x)
@@ -1545,7 +1545,7 @@ val NOT_EXISTS_THM = thm (#(FNAME), #(LINE))("NOT_EXISTS_THM",
 (* FORALL_AND_THM |- !P Q. (!x. P x /\ Q x) = ((!x. P x) /\ (!x. Q x))       *)
 (* ------------------------------------------------------------------------- *)
 
-val FORALL_AND_THM = thm (#(FNAME), #(LINE))("FORALL_AND_THM",
+val FORALL_AND_THM = thm (#(FILE), #(LINE))("FORALL_AND_THM",
     let val f = “P:'a->bool”
         val g = “Q:'a->bool”
         val x = “x:'a”
@@ -1561,7 +1561,7 @@ val FORALL_AND_THM = thm (#(FNAME), #(LINE))("FORALL_AND_THM",
 (* LEFT_AND_FORALL_THM = |- !P Q. (!x. P x) /\ Q = (!x. P x /\ Q)            *)
 (* ------------------------------------------------------------------------- *)
 
-val LEFT_AND_FORALL_THM = thm (#(FNAME), #(LINE))("LEFT_AND_FORALL_THM",
+val LEFT_AND_FORALL_THM = thm (#(FILE), #(LINE))("LEFT_AND_FORALL_THM",
     let val x = “x:'a”
         val f = “P:'a->bool”
         val Q = “Q:bool”
@@ -1577,7 +1577,7 @@ val LEFT_AND_FORALL_THM = thm (#(FNAME), #(LINE))("LEFT_AND_FORALL_THM",
 (* RIGHT_AND_FORALL_THM = |- !P Q. P /\ (!x. Q x) = (!x. P /\ Q x)           *)
 (* ------------------------------------------------------------------------- *)
 
-val RIGHT_AND_FORALL_THM = thm (#(FNAME), #(LINE))("RIGHT_AND_FORALL_THM",
+val RIGHT_AND_FORALL_THM = thm (#(FILE), #(LINE))("RIGHT_AND_FORALL_THM",
     let val x = “x:'a”
         val P = “P:bool”
         val g = “Q:'a->bool”
@@ -1593,7 +1593,7 @@ val RIGHT_AND_FORALL_THM = thm (#(FNAME), #(LINE))("RIGHT_AND_FORALL_THM",
 (* EXISTS_OR_THM |- !P Q. (?x. P x \/ Q x) = ((?x. P x) \/ (?x. Q x))        *)
 (* ------------------------------------------------------------------------- *)
 
-val EXISTS_OR_THM = thm (#(FNAME), #(LINE))("EXISTS_OR_THM",
+val EXISTS_OR_THM = thm (#(FILE), #(LINE))("EXISTS_OR_THM",
     let val f = “P:'a->bool”
         val g = “Q:'a->bool”
         val x = “x:'a”
@@ -1619,7 +1619,7 @@ val EXISTS_OR_THM = thm (#(FNAME), #(LINE))("EXISTS_OR_THM",
 (* LEFT_OR_EXISTS_THM = |- (?x. P x) \/ Q = (?x. P x \/ Q)                   *)
 (* ------------------------------------------------------------------------- *)
 
-val LEFT_OR_EXISTS_THM = thm (#(FNAME), #(LINE))("LEFT_OR_EXISTS_THM",
+val LEFT_OR_EXISTS_THM = thm (#(FILE), #(LINE))("LEFT_OR_EXISTS_THM",
     let val x = “x:'a”
         val Q = “Q:bool”
         val f = “P:'a->bool”
@@ -1643,7 +1643,7 @@ val LEFT_OR_EXISTS_THM = thm (#(FNAME), #(LINE))("LEFT_OR_EXISTS_THM",
 (* RIGHT_OR_EXISTS_THM = |- P \/ (?x. Q x) = (?x. P \/ Q x)                  *)
 (* ------------------------------------------------------------------------- *)
 
-val RIGHT_OR_EXISTS_THM = thm (#(FNAME), #(LINE))("RIGHT_OR_EXISTS_THM",
+val RIGHT_OR_EXISTS_THM = thm (#(FILE), #(LINE))("RIGHT_OR_EXISTS_THM",
     let val x = “x:'a”
         val P = “P:bool”
         val g = “Q:'a->bool”
@@ -1666,7 +1666,7 @@ val RIGHT_OR_EXISTS_THM = thm (#(FNAME), #(LINE))("RIGHT_OR_EXISTS_THM",
 (* BOTH_EXISTS_AND_THM = |- !P Q. (?x. P /\ Q) = (?x. P) /\ (?x. Q)          *)
 (* ------------------------------------------------------------------------- *)
 
-val BOTH_EXISTS_AND_THM = thm (#(FNAME), #(LINE))("BOTH_EXISTS_AND_THM",
+val BOTH_EXISTS_AND_THM = thm (#(FILE), #(LINE))("BOTH_EXISTS_AND_THM",
     let val x = “x:'a”
         val P = “P:bool”
         val Q = “Q:bool”
@@ -1693,7 +1693,7 @@ val BOTH_EXISTS_AND_THM = thm (#(FNAME), #(LINE))("BOTH_EXISTS_AND_THM",
 (* LEFT_EXISTS_AND_THM = |- !P Q. (?x. P x /\ Q) = (?x. P x) /\ Q            *)
 (* ------------------------------------------------------------------------- *)
 
-val LEFT_EXISTS_AND_THM = thm (#(FNAME), #(LINE))("LEFT_EXISTS_AND_THM",
+val LEFT_EXISTS_AND_THM = thm (#(FILE), #(LINE))("LEFT_EXISTS_AND_THM",
     let val x = “x:'a”
         val f = “P:'a->bool”
         val P = mk_comb(f,x)
@@ -1720,7 +1720,7 @@ val LEFT_EXISTS_AND_THM = thm (#(FNAME), #(LINE))("LEFT_EXISTS_AND_THM",
 (* RIGHT_EXISTS_AND_THM = |- !P Q. (?x. P /\ Q x) = P /\ (?x. Q x)           *)
 (* ------------------------------------------------------------------------- *)
 
-val RIGHT_EXISTS_AND_THM = thm (#(FNAME), #(LINE))("RIGHT_EXISTS_AND_THM",
+val RIGHT_EXISTS_AND_THM = thm (#(FILE), #(LINE))("RIGHT_EXISTS_AND_THM",
     let val x = “x:'a”
         val P = “P:bool”
         val g = “Q:'a->bool”
@@ -1746,7 +1746,7 @@ val RIGHT_EXISTS_AND_THM = thm (#(FNAME), #(LINE))("RIGHT_EXISTS_AND_THM",
 (* BOTH_FORALL_OR_THM = |- !P Q. (!x. P \/ Q) = (!x. P) \/ (!x. Q)           *)
 (* ------------------------------------------------------------------------- *)
 
-val BOTH_FORALL_OR_THM = thm (#(FNAME), #(LINE))("BOTH_FORALL_OR_THM",
+val BOTH_FORALL_OR_THM = thm (#(FILE), #(LINE))("BOTH_FORALL_OR_THM",
   let val x = “x:'a”
       val P = “P:bool”
       val Q = “Q:bool”
@@ -1766,7 +1766,7 @@ val BOTH_FORALL_OR_THM = thm (#(FNAME), #(LINE))("BOTH_FORALL_OR_THM",
 (* LEFT_FORALL_OR_THM = |- !P Q. (!x. P x \/ Q) = (!x. P x) \/ Q             *)
 (* ------------------------------------------------------------------------- *)
 
-val LEFT_FORALL_OR_THM = thm (#(FNAME), #(LINE))("LEFT_FORALL_OR_THM",
+val LEFT_FORALL_OR_THM = thm (#(FILE), #(LINE))("LEFT_FORALL_OR_THM",
   let val x = “x:'a”
       val f = “P:'a->bool”
       val P = mk_comb(f,x)
@@ -1789,7 +1789,7 @@ val LEFT_FORALL_OR_THM = thm (#(FNAME), #(LINE))("LEFT_FORALL_OR_THM",
 (* RIGHT_FORALL_OR_THM = |- !P Q. (!x. P \/ Q x) = P \/ (!x. Q x)            *)
 (* ------------------------------------------------------------------------- *)
 
-val RIGHT_FORALL_OR_THM = thm (#(FNAME), #(LINE))("RIGHT_FORALL_OR_THM",
+val RIGHT_FORALL_OR_THM = thm (#(FILE), #(LINE))("RIGHT_FORALL_OR_THM",
     let val x = “x:'a”
         val P = “P:bool”
         val g = “Q:'a->bool”
@@ -1813,7 +1813,7 @@ val RIGHT_FORALL_OR_THM = thm (#(FNAME), #(LINE))("RIGHT_FORALL_OR_THM",
 (* BOTH_FORALL_IMP_THM = |- (!x. P ==> Q) = ((?x.P) ==> (!x.Q))              *)
 (* ------------------------------------------------------------------------- *)
 
-val BOTH_FORALL_IMP_THM = thm (#(FNAME), #(LINE))("BOTH_FORALL_IMP_THM",
+val BOTH_FORALL_IMP_THM = thm (#(FILE), #(LINE))("BOTH_FORALL_IMP_THM",
     let val x = “x:'a”
         val P = “P:bool”
         val Q = “Q:bool”
@@ -1832,7 +1832,7 @@ val BOTH_FORALL_IMP_THM = thm (#(FNAME), #(LINE))("BOTH_FORALL_IMP_THM",
 (* LEFT_FORALL_IMP_THM = |- (!x. P[x]==>Q) = ((?x.P[x]) ==> Q)               *)
 (* ------------------------------------------------------------------------- *)
 
-val LEFT_FORALL_IMP_THM = thm (#(FNAME), #(LINE))("LEFT_FORALL_IMP_THM",
+val LEFT_FORALL_IMP_THM = thm (#(FILE), #(LINE))("LEFT_FORALL_IMP_THM",
     let val x = “x:'a”
         val f = “P:'a->bool”
         val P = mk_comb(f,x)
@@ -1852,7 +1852,7 @@ val LEFT_FORALL_IMP_THM = thm (#(FNAME), #(LINE))("LEFT_FORALL_IMP_THM",
 (* RIGHT_FORALL_IMP_THM = |- (!x. P==>Q[x]) = (P ==> (!x.Q[x]))              *)
 (* ------------------------------------------------------------------------- *)
 
-val RIGHT_FORALL_IMP_THM = thm (#(FNAME), #(LINE))("RIGHT_FORALL_IMP_THM",
+val RIGHT_FORALL_IMP_THM = thm (#(FILE), #(LINE))("RIGHT_FORALL_IMP_THM",
     let val x = “x:'a”
         val P = “P:bool”
         val g = “Q:'a->bool”
@@ -1869,7 +1869,7 @@ val RIGHT_FORALL_IMP_THM = thm (#(FNAME), #(LINE))("RIGHT_FORALL_IMP_THM",
 (* BOTH_EXISTS_IMP_THM = |- (?x. P ==> Q) = ((!x.P) ==> (?x.Q))              *)
 (* ------------------------------------------------------------------------- *)
 
-val BOTH_EXISTS_IMP_THM = thm (#(FNAME), #(LINE))("BOTH_EXISTS_IMP_THM",
+val BOTH_EXISTS_IMP_THM = thm (#(FILE), #(LINE))("BOTH_EXISTS_IMP_THM",
     let val x = “x:'a”
         val P = “P:bool”
         val Q = “Q:bool”
@@ -1890,7 +1890,7 @@ val BOTH_EXISTS_IMP_THM = thm (#(FNAME), #(LINE))("BOTH_EXISTS_IMP_THM",
 (* LEFT_EXISTS_IMP_THM = |- (?x. P[x] ==> Q) = ((!x.P[x]) ==> Q)             *)
 (* ------------------------------------------------------------------------- *)
 
-val LEFT_EXISTS_IMP_THM = thm (#(FNAME), #(LINE))("LEFT_EXISTS_IMP_THM",
+val LEFT_EXISTS_IMP_THM = thm (#(FILE), #(LINE))("LEFT_EXISTS_IMP_THM",
     let val x = “x:'a”
         val f = “P:'a->bool”
         val P = mk_comb(f,x)
@@ -1918,7 +1918,7 @@ val LEFT_EXISTS_IMP_THM = thm (#(FNAME), #(LINE))("LEFT_EXISTS_IMP_THM",
 (* RIGHT_EXISTS_IMP_THM = |- (?x. P ==> Q[x]) = (P ==> (?x.Q[x]))            *)
 (* ------------------------------------------------------------------------- *)
 
-val RIGHT_EXISTS_IMP_THM = thm (#(FNAME), #(LINE))("RIGHT_EXISTS_IMP_THM",
+val RIGHT_EXISTS_IMP_THM = thm (#(FILE), #(LINE))("RIGHT_EXISTS_IMP_THM",
     let val x = “x:'a”
         val P = “P:bool”
         val g = “Q:'a->bool”
@@ -1941,7 +1941,7 @@ val RIGHT_EXISTS_IMP_THM = thm (#(FNAME), #(LINE))("RIGHT_EXISTS_IMP_THM",
 (* [TFM 90.06.28]                                                        *)
 (* --------------------------------------------------------------------- *)
 
-val OR_IMP_THM = thm (#(FNAME), #(LINE))("OR_IMP_THM",
+val OR_IMP_THM = thm (#(FILE), #(LINE))("OR_IMP_THM",
  let val t1 = “A:bool” and t2 = “B:bool”
      val asm1 = ASSUME “^t1 = (^t2 \/ ^t1)”
      and asm2 = EQT_INTRO(ASSUME t2)
@@ -1963,7 +1963,7 @@ val OR_IMP_THM = thm (#(FNAME), #(LINE))("OR_IMP_THM",
 (* [TFM 90.07.09]                                                        *)
 (* --------------------------------------------------------------------- *)
 
-val NOT_IMP = thm (#(FNAME), #(LINE))("NOT_IMP",
+val NOT_IMP = thm (#(FILE), #(LINE))("NOT_IMP",
 let val t1 = “A:bool” and t2 = “B:bool”
     val asm1 = ASSUME “~(^t1 ==> ^t2)”
     val thm1 = SUBST [t1 |-> EQF_INTRO (ASSUME (mk_neg t1))] (concl asm1) asm1
@@ -1985,7 +1985,7 @@ let val t1 = “A:bool” and t2 = “B:bool”
 (* DISJ_ASSOC: |- !A B C. A \/ B \/ C = (A \/ B) \/ C                    *)
 (* --------------------------------------------------------------------- *)
 
-val DISJ_ASSOC = thm (#(FNAME), #(LINE))("DISJ_ASSOC",
+val DISJ_ASSOC = thm (#(FILE), #(LINE))("DISJ_ASSOC",
 let val t1 = “A:bool” and t2 = “B:bool” and t3 = “C:bool”
     val at1 = DISJ1 (DISJ1 (ASSUME t1) t2) t3 and
         at2 = DISJ1 (DISJ2 t1 (ASSUME t2)) t3 and
@@ -2007,7 +2007,7 @@ let val t1 = “A:bool” and t2 = “B:bool” and t3 = “C:bool”
 (* DISJ_SYM: |- !A B. A \/ B = B \/ A                                    *)
 (* --------------------------------------------------------------------- *)
 
-val DISJ_SYM = thm (#(FNAME), #(LINE))("DISJ_SYM",
+val DISJ_SYM = thm (#(FILE), #(LINE))("DISJ_SYM",
 let val t1   = “A:bool” and t2 = “B:bool”
     val th1  = DISJ1 (ASSUME t1) t2 and th2 = DISJ2 t1 (ASSUME t2)
     val thm1 = DISJ_CASES (ASSUME(mk_disj(t2,t1))) th2 th1
@@ -2019,14 +2019,14 @@ let val t1   = “A:bool” and t2 = “B:bool”
    GENL [t1,t2] (IMP_ANTISYM_RULE imp2 imp1)
  end);
 
-val _ = thm (#(FNAME), #(LINE))("DISJ_COMM", DISJ_SYM);
+val _ = thm (#(FILE), #(LINE))("DISJ_COMM", DISJ_SYM);
 
 (* --------------------------------------------------------------------- *)
 (* DE_MORGAN_THM:                                                        *)
 (*  |- !A B. (~(t1 /\ t2) = ~t1 \/ ~t2) /\ (~(t1 \/ t2) = ~t1 /\ ~t2)    *)
 (* --------------------------------------------------------------------- *)
 
-val DE_MORGAN_THM = thm (#(FNAME), #(LINE))("DE_MORGAN_THM",
+val DE_MORGAN_THM = thm (#(FILE), #(LINE))("DE_MORGAN_THM",
 let val t1 = “A:bool” and t2 = “B:bool”
     val thm1 =
       let val asm1 = ASSUME “~(^t1 /\ ^t2)”
@@ -2080,7 +2080,7 @@ let val t1 = “A:bool” and t2 = “B:bool”
 (* RIGHT_OR_OVER_AND  |- !A B C. B /\ C \/ A = (B \/ A) /\ (C \/ A)         *)
 (* -------------------------------------------------------------------------*)
 
-val LEFT_AND_OVER_OR = thm (#(FNAME), #(LINE))("LEFT_AND_OVER_OR",
+val LEFT_AND_OVER_OR = thm (#(FILE), #(LINE))("LEFT_AND_OVER_OR",
     let val t1 = “A:bool”
         and t2 = “B:bool”
         and t3 = “C:bool”
@@ -2097,7 +2097,7 @@ val LEFT_AND_OVER_OR = thm (#(FNAME), #(LINE))("LEFT_AND_OVER_OR",
       GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2)))
     end);
 
-val RIGHT_AND_OVER_OR = thm (#(FNAME), #(LINE))("RIGHT_AND_OVER_OR",
+val RIGHT_AND_OVER_OR = thm (#(FILE), #(LINE))("RIGHT_AND_OVER_OR",
    let val t1 = “A:bool”
        and t2 = “B:bool”
        and t3 = “C:bool”
@@ -2114,7 +2114,7 @@ val RIGHT_AND_OVER_OR = thm (#(FNAME), #(LINE))("RIGHT_AND_OVER_OR",
      GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2)))
    end);
 
-val LEFT_OR_OVER_AND = thm (#(FNAME), #(LINE))("LEFT_OR_OVER_AND",
+val LEFT_OR_OVER_AND = thm (#(FILE), #(LINE))("LEFT_OR_OVER_AND",
    let val t1 = “A:bool”
        and t2 = “B:bool”
        and t3 = “C:bool”
@@ -2133,7 +2133,7 @@ val LEFT_OR_OVER_AND = thm (#(FNAME), #(LINE))("LEFT_OR_OVER_AND",
      GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2)))
    end);
 
-val RIGHT_OR_OVER_AND = thm (#(FNAME), #(LINE))("RIGHT_OR_OVER_AND",
+val RIGHT_OR_OVER_AND = thm (#(FILE), #(LINE))("RIGHT_OR_OVER_AND",
    let val t1 = “A:bool”
        and t2 = “B:bool”
        and t3 = “C:bool”
@@ -2156,7 +2156,7 @@ val RIGHT_OR_OVER_AND = thm (#(FNAME), #(LINE))("RIGHT_OR_OVER_AND",
  * IMP_DISJ_THM = |- !A B. A ==> B = ~A \/ B                                 *
  *---------------------------------------------------------------------------*)
 
-val IMP_DISJ_THM = thm (#(FNAME), #(LINE))("IMP_DISJ_THM",
+val IMP_DISJ_THM = thm (#(FILE), #(LINE))("IMP_DISJ_THM",
 let val A = “A:bool”
     val B = “B:bool”
     val th1 = ASSUME “A ==> B”
@@ -2210,7 +2210,7 @@ val DISJ_IMP_THM = let
   val r_from_q = MP q_imp_r ass_Q
   val rl_imp = DISCH rhs (DISCH porq (DISJ_CASES ass_porq r_from_p r_from_q))
 in
-  thm (#(FNAME), #(LINE))("DISJ_IMP_THM",
+  thm (#(FILE), #(LINE))("DISJ_IMP_THM",
                           GENL [P,Q,R] (IMP_ANTISYM_RULE lr_imp rl_imp))
 end
 
@@ -2242,7 +2242,7 @@ val IMP_CONJ_THM = let
   val QaR_th = CONJ Q_th R_th
   val R2L = DISCH PiQaPiR (DISCH P QaR_th)
 in
-  thm (#(FNAME), #(LINE))("IMP_CONJ_THM",
+  thm (#(FILE), #(LINE))("IMP_CONJ_THM",
                           GENL [P,Q,R] (IMP_ANTISYM_RULE L2R R2L))
 end
 
@@ -2259,7 +2259,7 @@ local fun nthCONJUNCT n cth =
            then CONJUNCT1 th else th
         end
 in
-val IMP_F_EQ_F = thm (#(FNAME), #(LINE))("IMP_F_EQ_F",
+val IMP_F_EQ_F = thm (#(FILE), #(LINE))("IMP_F_EQ_F",
    GEN “t:bool”
      (TRANS (nthCONJUNCT 5 (SPEC_ALL IMP_CLAUSES))
             (SYM (nthCONJUNCT 4 (SPEC_ALL EQ_CLAUSES)))))
@@ -2272,7 +2272,7 @@ end;
 (*                                                         RJB 92.09.26 *)
 (* ---------------------------------------------------------------------*)
 
-val AND_IMP_INTRO = thm (#(FNAME), #(LINE))("AND_IMP_INTRO",
+val AND_IMP_INTRO = thm (#(FILE), #(LINE))("AND_IMP_INTRO",
 let val t1 = “t1:bool”
     and t2 = “t2:bool”
     and t3 = “t3:bool”
@@ -2302,7 +2302,7 @@ let val t1 = “t1:bool”
 (*                                                         RJB 92.09.26 *)
 (* ---------------------------------------------------------------------*)
 
-val EQ_IMP_THM = thm (#(FNAME), #(LINE))("EQ_IMP_THM",
+val EQ_IMP_THM = thm (#(FILE), #(LINE))("EQ_IMP_THM",
 let val t1 = “t1:bool”
     and t2 = “t2:bool”
     val conj = “$/\”
@@ -2331,7 +2331,7 @@ let val t1 = “t1:bool”
 (*                                                         RJB 92.09.26 *)
 (* ---------------------------------------------------------------------*)
 
-val EQ_EXPAND = thm (#(FNAME), #(LINE))("EQ_EXPAND",
+val EQ_EXPAND = thm (#(FILE), #(LINE))("EQ_EXPAND",
 let val t1 = “t1:bool” and t2 = “t2:bool”
     val conj = “$/\”   and disj = “$\/”
     val [NOT1,NOT2] = tl (CONJUNCTS NOT_CLAUSES)
@@ -2365,7 +2365,7 @@ let val t1 = “t1:bool” and t2 = “t2:bool”
 (*                                                         RJB 92.09.26 *)
 (* ---------------------------------------------------------------------*)
 
-val COND_RATOR = thm (#(FNAME), #(LINE))("COND_RATOR",
+val COND_RATOR = thm (#(FILE), #(LINE))("COND_RATOR",
 let val f = “f: 'a -> 'b”
     val g = “g: 'a -> 'b”
     val x = “x:'a”
@@ -2400,7 +2400,7 @@ let val f = “f: 'a -> 'b”
 (*                                                         RJB 92.09.26 *)
 (* ---------------------------------------------------------------------*)
 
-val COND_RAND = thm (#(FNAME), #(LINE))("COND_RAND",
+val COND_RAND = thm (#(FILE), #(LINE))("COND_RAND",
 let val f = “f: 'a -> 'b”
     val x = “x:'a”
     val y = “y:'a”
@@ -2434,7 +2434,7 @@ let val f = “f: 'a -> 'b”
 (*                                                         RJB 92.09.26 *)
 (* ---------------------------------------------------------------------*)
 
-val COND_ABS = thm (#(FNAME), #(LINE))("COND_ABS",
+val COND_ABS = thm (#(FILE), #(LINE))("COND_ABS",
 let val b = “b:bool”
     val f = “f:'a->'b”
     val g = “g:'a->'b”
@@ -2453,7 +2453,7 @@ let val b = “b:bool”
 (*                                                         RJB 92.09.26 *)
 (* ---------------------------------------------------------------------*)
 
-val COND_EXPAND = thm (#(FNAME), #(LINE))("COND_EXPAND",
+val COND_EXPAND = thm (#(FILE), #(LINE))("COND_EXPAND",
 let val b    = “b:bool”
     val t1   = “t1:bool”
     val t2   = “t2:bool”
@@ -2500,7 +2500,7 @@ let val b    = “b:bool”
 (*                                                          TT 09.03.18 *)
 (* ---------------------------------------------------------------------*)
 
-val COND_EXPAND_IMP = thm (#(FNAME), #(LINE))("COND_EXPAND_IMP",
+val COND_EXPAND_IMP = thm (#(FILE), #(LINE))("COND_EXPAND_IMP",
 let val b    = “b:bool”
     val t1   = “t1:bool”
     val t2   = “t2:bool”
@@ -2528,7 +2528,7 @@ end);
 (*                                                          TT 09.03.18 *)
 (* ---------------------------------------------------------------------*)
 
-val COND_EXPAND_OR = thm (#(FNAME), #(LINE))("COND_EXPAND_OR",
+val COND_EXPAND_OR = thm (#(FILE), #(LINE))("COND_EXPAND_OR",
 let val b    = “b:bool”
     val t1   = “t1:bool”
     val t2   = “t2:bool”
@@ -2568,7 +2568,7 @@ let val b    = “b:bool”
  end);
 
 
-val TYPE_DEFINITION_THM = thm (#(FNAME), #(LINE))("TYPE_DEFINITION_THM",
+val TYPE_DEFINITION_THM = thm (#(FILE), #(LINE))("TYPE_DEFINITION_THM",
   let val P   = “P:'a-> bool”
       val rep = “rep :'b -> 'a”
   in
@@ -2577,14 +2577,14 @@ val TYPE_DEFINITION_THM = thm (#(FNAME), #(LINE))("TYPE_DEFINITION_THM",
           (RIGHT_BETA (AP_THM TYPE_DEFINITION P)) rep)))
   end);
 
-val ONTO_THM = thm (#(FNAME), #(LINE))(
+val ONTO_THM = thm (#(FILE), #(LINE))(
   "ONTO_THM",
   let val f = mk_var("f", Type.alpha --> Type.beta)
   in
       GEN f (RIGHT_BETA (AP_THM ONTO_DEF f))
   end);
 
-val ONE_ONE_THM = thm (#(FNAME), #(LINE))(
+val ONE_ONE_THM = thm (#(FILE), #(LINE))(
   "ONE_ONE_THM",
   let val f = mk_var("f", Type.alpha --> Type.beta)
   in
@@ -2597,7 +2597,7 @@ val ONE_ONE_THM = thm (#(FNAME), #(LINE))(
  *         ?rep abs. (!a. abs (rep a) = a) /\ !r. P r = (rep (abs r) = r)    *
  *---------------------------------------------------------------------------*)
 
-val ABS_REP_THM = thm (#(FNAME), #(LINE))("ABS_REP_THM",
+val ABS_REP_THM = thm (#(FILE), #(LINE))("ABS_REP_THM",
    let val th1 = ASSUME “?rep:'b->'a. TYPE_DEFINITION P rep”
        val th2 = MK_EXISTS (SPEC “P:'a->bool” TYPE_DEFINITION_THM)
        val def = EQ_MP th2 th1
@@ -2643,7 +2643,7 @@ val ABS_REP_THM = thm (#(FNAME), #(LINE))("ABS_REP_THM",
     LET_RAND =  P (let x = M in N x) = (let x = M in P (N x))
  ---------------------------------------------------------------------------*)
 
-val LET_RAND = thm (#(FNAME), #(LINE))("LET_RAND",
+val LET_RAND = thm (#(FILE), #(LINE))("LET_RAND",
  let val tm1 = “\x:'a. P (N x:'b):bool”
      val tm2 = “M:'a”
      val tm3 = “\x:'a. N x:'b”
@@ -2659,7 +2659,7 @@ val LET_RAND = thm (#(FNAME), #(LINE))("LET_RAND",
     LET_RATOR =  (let x = M in N x) b = (let x = M in N x b)
  ---------------------------------------------------------------------------*)
 
-val LET_RATOR = thm (#(FNAME), #(LINE))("LET_RATOR",
+val LET_RATOR = thm (#(FILE), #(LINE))("LET_RATOR",
  let val M = “M:'a”
      val b = “b:'b”
      val tm1 = “\x:'a. N x:'b->'c”
@@ -2676,7 +2676,7 @@ val LET_RATOR = thm (#(FNAME), #(LINE))("LET_RATOR",
            !P. (!x y. P x y) = (!y x. P x y)
  ---------------------------------------------------------------------------*)
 
-val SWAP_FORALL_THM = thm (#(FNAME), #(LINE))("SWAP_FORALL_THM",
+val SWAP_FORALL_THM = thm (#(FILE), #(LINE))("SWAP_FORALL_THM",
   let val P = mk_var("P", “:'a->'b->bool”)
       val x = mk_var("x", Type.alpha)
       val y = mk_var("y", Type.beta)
@@ -2693,7 +2693,7 @@ val SWAP_FORALL_THM = thm (#(FNAME), #(LINE))("SWAP_FORALL_THM",
            !P. (?x y. P x y) = (?y x. P x y)
  ---------------------------------------------------------------------------*)
 
-val SWAP_EXISTS_THM = thm (#(FNAME), #(LINE))("SWAP_EXISTS_THM",
+val SWAP_EXISTS_THM = thm (#(FILE), #(LINE))("SWAP_EXISTS_THM",
   let val P = mk_var("P", “:'a->'b->bool”)
       val x = mk_var("x", Type.alpha)
       val y = mk_var("y", Type.beta)
@@ -2721,7 +2721,7 @@ val SWAP_EXISTS_THM = thm (#(FNAME), #(LINE))("SWAP_EXISTS_THM",
      (?!x. P x) = (?x. P x) /\ (!x y. P x /\ P y ==> (x = y))
  ---------------------------------------------------------------------------*)
 
-val EXISTS_UNIQUE_THM = thm (#(FNAME), #(LINE))("EXISTS_UNIQUE_THM",
+val EXISTS_UNIQUE_THM = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_THM",
  let val th1 = RIGHT_BETA (AP_THM EXISTS_UNIQUE_DEF “\x:'a. P x:bool”)
      val th2 = CONV_RULE (RAND_CONV (RAND_CONV
                 (QUANT_CONV (QUANT_CONV (RATOR_CONV
@@ -2737,7 +2737,7 @@ val EXISTS_UNIQUE_THM = thm (#(FNAME), #(LINE))("EXISTS_UNIQUE_THM",
     |- !P. (?!x. P x) <=> ?x. !y. P y <=> (y = x)
    ---------------------------------------------------------------------- *)
 
-val EXISTS_UNIQUE_ALT' = thm (#(FNAME), #(LINE))(
+val EXISTS_UNIQUE_ALT' = thm (#(FILE), #(LINE))(
   "EXISTS_UNIQUE_ALT'",
   let
     val eu_r = ASSUME (rhs (concl EXISTS_UNIQUE_THM))
@@ -2777,7 +2777,7 @@ val EXISTS_UNIQUE_ALT' = thm (#(FNAME), #(LINE))(
                    (LET f M = LET g N)
  ---------------------------------------------------------------------------*)
 
-val LET_CONG = thm (#(FNAME), #(LINE))("LET_CONG",
+val LET_CONG = thm (#(FILE), #(LINE))("LET_CONG",
   let val f = mk_var("f",alpha-->beta)
       val g = mk_var("g",alpha-->beta)
       val M = mk_var("M",alpha)
@@ -2807,7 +2807,7 @@ val LET_CONG = thm (#(FNAME), #(LINE))("LET_CONG",
                    (x ==> y = x' ==> y')
  ---------------------------------------------------------------------------*)
 
-val IMP_CONG = thm (#(FNAME), #(LINE))("IMP_CONG",
+val IMP_CONG = thm (#(FILE), #(LINE))("IMP_CONG",
  let val x = mk_var("x",Type.bool)
      val x' = mk_var("x'",Type.bool)
      val y = mk_var("y",Type.bool)
@@ -2837,7 +2837,7 @@ val IMP_CONG = thm (#(FNAME), #(LINE))("IMP_CONG",
                             (P /\ Q = P' /\ Q')
  ---------------------------------------------------------------------------*)
 
-val AND_CONG = thm (#(FNAME), #(LINE))("AND_CONG",
+val AND_CONG = thm (#(FILE), #(LINE))("AND_CONG",
  let val P = mk_var("P",Type.bool)
      val P' = mk_var("P'",Type.bool)
      val Q = mk_var("Q",Type.bool)
@@ -2869,7 +2869,7 @@ val AND_CONG = thm (#(FNAME), #(LINE))("AND_CONG",
           (P /\ Q = P' /\ Q')
  ---------------------------------------------------------------------------*)
 
-val LEFT_AND_CONG = thm (#(FNAME), #(LINE))("LEFT_AND_CONG",
+val LEFT_AND_CONG = thm (#(FILE), #(LINE))("LEFT_AND_CONG",
  let val P = mk_var("P",Type.bool)
      val P' = mk_var("P'",Type.bool)
      val Q = mk_var("Q",Type.bool)
@@ -2902,7 +2902,7 @@ val LEFT_AND_CONG = thm (#(FNAME), #(LINE))("LEFT_AND_CONG",
                    (P \/ Q = P' \/ Q')
  ---------------------------------------------------------------------------*)
 
-val OR_CONG = thm (#(FNAME), #(LINE))("OR_CONG",
+val OR_CONG = thm (#(FILE), #(LINE))("OR_CONG",
  let val P = mk_var("P",Type.bool)
      val P' = mk_var("P'",Type.bool)
      val Q = mk_var("Q",Type.bool)
@@ -2955,7 +2955,7 @@ val OR_CONG = thm (#(FNAME), #(LINE))("OR_CONG",
           (P \/ Q = P' \/ Q')
  ---------------------------------------------------------------------------*)
 
-val LEFT_OR_CONG = thm (#(FNAME), #(LINE))("LEFT_OR_CONG",
+val LEFT_OR_CONG = thm (#(FILE), #(LINE))("LEFT_OR_CONG",
  let fun mk_boolvar s = mk_var(s,Type.bool)
      val [P,P',Q,Q'] = map mk_boolvar ["P","P'","Q","Q'"]
      val notP = mk_neg P
@@ -2992,7 +2992,7 @@ val LEFT_OR_CONG = thm (#(FNAME), #(LINE))("LEFT_OR_CONG",
 
 fun mk_cond {cond,larm,rarm} = “if ^cond then ^larm else ^rarm”;
 
-val COND_CONG = thm (#(FNAME), #(LINE))("COND_CONG",
+val COND_CONG = thm (#(FILE), #(LINE))("COND_CONG",
  let val P = mk_var("P",Type.bool)
      val Q = mk_var("Q",Type.bool)
      val x = mk_var("x",alpha)
@@ -3122,9 +3122,9 @@ val (RES_FORALL_CONG, RES_EXISTS_CONG) = let
   val ex_eqn = IMP_ANTISYM_RULE ex_pf_imp_qg ex_qg_imp_pf
 
 in
-  (thm (#(FNAME), #(LINE))("RES_FORALL_CONG",
+  (thm (#(FILE), #(LINE))("RES_FORALL_CONG",
                            DISCH PeqQ_t (DISCH feqg_t fa_eqn)),
-   thm (#(FNAME), #(LINE))("RES_EXISTS_CONG",
+   thm (#(FILE), #(LINE))("RES_EXISTS_CONG",
                            DISCH PeqQ_t (DISCH feqg_t ex_eqn)))
 end
 
@@ -3137,7 +3137,7 @@ end
 (* MONO_AND |- (x ==> y) /\ (z ==> w) ==> (x /\ z ==> y /\ w)                *)
 (* ------------------------------------------------------------------------- *)
 
-val MONO_AND = thm (#(FNAME), #(LINE))("MONO_AND",
+val MONO_AND = thm (#(FILE), #(LINE))("MONO_AND",
  let val tm1 = “x ==> y”
      val tm2 = “z ==> w”
      val tm3 = “x /\ z”
@@ -3160,7 +3160,7 @@ val MONO_AND = thm (#(FNAME), #(LINE))("MONO_AND",
 (* MONO_OR |- (x ==> y) /\ (z ==> w) ==> (x \/ z ==> y \/ w)                 *)
 (* ------------------------------------------------------------------------- *)
 
-val MONO_OR = thm (#(FNAME), #(LINE))("MONO_OR",
+val MONO_OR = thm (#(FILE), #(LINE))("MONO_OR",
  let val tm1 = “x ==> y”
      val tm2 = “z ==> w”
      val tm3 = “x \/ z”
@@ -3181,7 +3181,7 @@ val MONO_OR = thm (#(FNAME), #(LINE))("MONO_OR",
 (* MONO_IMP |- (y ==> x) /\ (z ==> w) ==> ((x ==> z) ==> (y ==> w))          *)
 (* ------------------------------------------------------------------------- *)
 
-val MONO_IMP = thm (#(FNAME), #(LINE))("MONO_IMP",
+val MONO_IMP = thm (#(FILE), #(LINE))("MONO_IMP",
  let val tm1 = “y ==> x”
      val tm2 = “z ==> w”
      val tm3 = “x ==> z”
@@ -3203,7 +3203,7 @@ val MONO_IMP = thm (#(FNAME), #(LINE))("MONO_IMP",
 (* MONO_NOT |- (y ==> x) ==> (~x ==> ~y)                                     *)
 (* ------------------------------------------------------------------------- *)
 
-val MONO_NOT = thm (#(FNAME), #(LINE))("MONO_NOT",
+val MONO_NOT = thm (#(FILE), #(LINE))("MONO_NOT",
  let val tm1 = “y ==> x”
      val tm2 = “~x”
      val tm3 = “y:bool”
@@ -3221,7 +3221,7 @@ val MONO_NOT = thm (#(FNAME), #(LINE))("MONO_NOT",
 (* MONO_NOT_EQ |- (y ==> x) = (~x ==> ~y)                                     *)
 (* ------------------------------------------------------------------------- *)
 
-val MONO_NOT_EQ = thm (#(FNAME), #(LINE))("MONO_NOT_EQ",
+val MONO_NOT_EQ = thm (#(FILE), #(LINE))("MONO_NOT_EQ",
  let val tm1 = “x:bool”
      val tm2 = “y:bool”
      val th1 = INST [tm1 |-> mk_neg tm2, tm2 |-> mk_neg tm1] MONO_NOT
@@ -3239,7 +3239,7 @@ val MONO_NOT_EQ = thm (#(FNAME), #(LINE))("MONO_NOT_EQ",
 (* MONO_ALL |- (!x. P x ==> Q x) ==> (!x. P x) ==> !x. Q x                   *)
 (* ------------------------------------------------------------------------- *)
 
-val MONO_ALL = thm (#(FNAME), #(LINE))("MONO_ALL",
+val MONO_ALL = thm (#(FILE), #(LINE))("MONO_ALL",
  let val tm1 = “!x:'a. P x ==> Q x”
      val tm2 = “!x:'a. P x”
      val tm3 = “x:'a”
@@ -3256,7 +3256,7 @@ val MONO_ALL = thm (#(FNAME), #(LINE))("MONO_ALL",
 (* MONO_EXISTS =  [] |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x          *)
 (* ------------------------------------------------------------------------- *)
 
-val MONO_EXISTS = thm (#(FNAME), #(LINE))("MONO_EXISTS",
+val MONO_EXISTS = thm (#(FILE), #(LINE))("MONO_EXISTS",
  let val tm1 = “!x:'a. P x ==> Q x”
      val tm2 = “?x:'a. P x”
      val tm3 = “@x:'a. P x”
@@ -3276,7 +3276,7 @@ val MONO_EXISTS = thm (#(FNAME), #(LINE))("MONO_EXISTS",
 (*              ==> (if b then x else z) ==> (if b then y else w)            *)
 (* ------------------------------------------------------------------------- *)
 
-val MONO_COND = thm (#(FNAME), #(LINE))("MONO_COND",
+val MONO_COND = thm (#(FILE), #(LINE))("MONO_COND",
  let val tm1 = “x ==> y”
      val tm2 = “z ==> w”
      val tm3 = “if b then x else z:bool”
@@ -3322,7 +3322,7 @@ val MONO_COND = thm (#(FNAME), #(LINE))("MONO_COND",
 (* EXISTS_REFL |- !a. ?x. x = a                                              *)
 (* ------------------------------------------------------------------------- *)
 
-val EXISTS_REFL = thm (#(FNAME), #(LINE))("EXISTS_REFL",
+val EXISTS_REFL = thm (#(FILE), #(LINE))("EXISTS_REFL",
  let val a = “a:'a”
      val th1 = REFL a
      val th2 = EXISTS (“?x:'a. x = a”, a) th1
@@ -3333,7 +3333,7 @@ val EXISTS_REFL = thm (#(FNAME), #(LINE))("EXISTS_REFL",
 (* EXISTS_UNIQUE_REFL |- !a. ?!x. x = a                                      *)
 (* ------------------------------------------------------------------------- *)
 
-val EXISTS_UNIQUE_REFL = thm (#(FNAME), #(LINE))("EXISTS_UNIQUE_REFL",
+val EXISTS_UNIQUE_REFL = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_REFL",
  let val a = “a:'a”
      val P = “\x:'a. x = a”
      val tmx = “^P x”
@@ -3362,7 +3362,7 @@ val EXISTS_UNIQUE_REFL = thm (#(FNAME), #(LINE))("EXISTS_UNIQUE_REFL",
     EXISTS_UNIQUE_FALSE |- (?!x. F) <=> F
    ---------------------------------------------------------------------- *)
 
-val EXISTS_UNIQUE_FALSE = thm (#(FNAME), #(LINE))("EXISTS_UNIQUE_FALSE",
+val EXISTS_UNIQUE_FALSE = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_FALSE",
   let
     val BINDER_CONV = RAND_CONV o ABS_CONV
     val LAND_CONV = RATOR_CONV o RAND_CONV
@@ -3388,7 +3388,7 @@ val EXISTS_UNIQUE_FALSE = thm (#(FNAME), #(LINE))("EXISTS_UNIQUE_FALSE",
 (* UNWIND1_THM |- !P a. (?x. (a = x) /\ P x) = P a                           *)
 (* ------------------------------------------------------------------------- *)
 
-val UNWIND_THM1 = thm (#(FNAME), #(LINE))("UNWIND_THM1",
+val UNWIND_THM1 = thm (#(FILE), #(LINE))("UNWIND_THM1",
  let val P = “P:'a->bool”
      val a = “a:'a”
      val Pa = “^P ^a”
@@ -3414,7 +3414,7 @@ val UNWIND_THM1 = thm (#(FNAME), #(LINE))("UNWIND_THM1",
 (* UNWIND_THM2  |- !P a. (?x. (x = a) /\ P x) = P a                          *)
 (* ------------------------------------------------------------------------- *)
 
-val UNWIND_THM2 = thm (#(FNAME), #(LINE))("UNWIND_THM2",
+val UNWIND_THM2 = thm (#(FILE), #(LINE))("UNWIND_THM2",
  let val P = “P:'a->bool”
      val a = “a:'a”
      val Px = “^P x”
@@ -3443,7 +3443,7 @@ val UNWIND_THM2 = thm (#(FNAME), #(LINE))("UNWIND_THM2",
 (* UNWIND_FORALL_THM1   |- !f v. (!x. (v = x) ==> f x) = f v                 *)
 (* ------------------------------------------------------------------------- *)
 
-val UNWIND_FORALL_THM1 = thm (#(FNAME), #(LINE))("UNWIND_FORALL_THM1",
+val UNWIND_FORALL_THM1 = thm (#(FILE), #(LINE))("UNWIND_FORALL_THM1",
  let val f = “f : 'a -> bool”
      val v = “v:'a”
      val fv = “^f ^v”
@@ -3465,7 +3465,7 @@ val UNWIND_FORALL_THM1 = thm (#(FNAME), #(LINE))("UNWIND_FORALL_THM1",
 (* UNWIND_FORALL_THM2   |- !f v. (!x. (x = v) ==> f x) = f v                 *)
 (* ------------------------------------------------------------------------- *)
 
-val UNWIND_FORALL_THM2 = thm (#(FNAME), #(LINE))("UNWIND_FORALL_THM2",
+val UNWIND_FORALL_THM2 = thm (#(FILE), #(LINE))("UNWIND_FORALL_THM2",
  let val f   = “f:'a->bool”
      val v   = “v:'a”
      val fv  = “^f ^v”
@@ -3487,7 +3487,7 @@ val UNWIND_FORALL_THM2 = thm (#(FNAME), #(LINE))("UNWIND_FORALL_THM2",
 (* Skolemization:    |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x)            *)
 (* ------------------------------------------------------------------------- *)
 
-val SKOLEM_THM = thm (#(FNAME), #(LINE))("SKOLEM_THM",
+val SKOLEM_THM = thm (#(FILE), #(LINE))("SKOLEM_THM",
  let val P = “P:'a -> 'b -> bool”
      val x = “x:'a”
      val y = “y:'b”
@@ -3531,7 +3531,7 @@ val SKOLEM_THM = thm (#(FNAME), #(LINE))("SKOLEM_THM",
 val bool_case_thm = let
   val (vs,_) = strip_forall (concl COND_CLAUSES)
 in
-  thm (#(FNAME), #(LINE))("bool_case_thm",
+  thm (#(FILE), #(LINE))("bool_case_thm",
            COND_CLAUSES |> SPECL vs |> CONJUNCTS |> map (GENL vs) |> LIST_CONJ)
 end
 
@@ -3539,14 +3539,14 @@ end
 (*    bool_case_ID = |- !x b. bool_case x x b = x                            *)
 (* ------------------------------------------------------------------------- *)
 
-val bool_case_ID = thm (#(FNAME), #(LINE))("bool_case_ID", COND_ID)
+val bool_case_ID = thm (#(FILE), #(LINE))("bool_case_ID", COND_ID)
 
 
 (* ------------------------------------------------------------------------- *)
 (* boolAxiom  |- !e0 e1. ?fn. (fn T = e0) /\ (fn F = e1)                     *)
 (* ------------------------------------------------------------------------- *)
 
-val boolAxiom = thm (#(FNAME), #(LINE))("boolAxiom",
+val boolAxiom = thm (#(FILE), #(LINE))("boolAxiom",
  let
    val ([e0,e1], _) = strip_forall (concl COND_CLAUSES)
    val (th2, th3) = CONJ_PAIR (SPECL [e0, e1] COND_CLAUSES)
@@ -3563,7 +3563,7 @@ val boolAxiom = thm (#(FNAME), #(LINE))("boolAxiom",
 (* bool_INDUCT |- !P. P T /\ P F ==> !b. P b                                 *)
 (* ------------------------------------------------------------------------- *)
 
-val bool_INDUCT = thm (#(FNAME), #(LINE))("bool_INDUCT",
+val bool_INDUCT = thm (#(FILE), #(LINE))("bool_INDUCT",
  let val P = “P:bool -> bool”
      val b = “b:bool”
      val v = “v:bool”
@@ -3587,9 +3587,9 @@ val bool_INDUCT = thm (#(FNAME), #(LINE))("bool_INDUCT",
          ((case P of T -> x || F -> y) = (case Q of T -> x' || F -> y'))
   --------------------------------------------------------------------------- *)
 
-val bool_case_CONG = thm (#(FNAME), #(LINE))("bool_case_CONG", COND_CONG)
+val bool_case_CONG = thm (#(FILE), #(LINE))("bool_case_CONG", COND_CONG)
 
-val FORALL_BOOL = thm (#(FNAME), #(LINE))
+val FORALL_BOOL = thm (#(FILE), #(LINE))
 ("FORALL_BOOL",
  let val tm1 = “!b:bool. P b”
      val tm2 = “P T /\ P F”
@@ -3675,7 +3675,7 @@ in
       DISJ2 uexP (EQ_MP uex_expanded (CONJ (ASSUME exQ) rhs))
     end
   in
-    thm (#(FNAME), #(LINE))(
+    thm (#(FILE), #(LINE))(
       "UEXISTS_OR_THM",
       GENL [P, Q] (DISCH_ALL (DISJ_CASES expq P_half Q_half))
     )
@@ -3721,7 +3721,7 @@ in
       mCONV_RULE (RAND_CONV (K pushx2)) exp6
     val mp' = Thm.INST [p |-> t, q |-> list_mk_forall [x,y] xeqy] pseudo_mp
   in
-    thm (#(FNAME), #(LINE))("UEXISTS_SIMP", mCONV_RULE (K mp') exp7)
+    thm (#(FILE), #(LINE))("UEXISTS_SIMP", mCONV_RULE (K mp') exp7)
   end
 end
 
@@ -3797,11 +3797,11 @@ val (RES_FORALL_THM, RES_EXISTS_THM, RES_EXISTS_UNIQUE_THM, RES_SELECT_THM) =
       fun mk_eq th =
           GENL Pf (List.foldl (RIGHT_BETA o uncurry (C AP_THM)) th Pf)
     in
-      (thm (#(FNAME), #(LINE))("RES_FORALL_THM", mk_eq RES_FORALL_DEF),
-       thm (#(FNAME), #(LINE))("RES_EXISTS_THM", mk_eq RES_EXISTS_DEF),
-       thm (#(FNAME), #(LINE))("RES_EXISTS_UNIQUE_THM",
+      (thm (#(FILE), #(LINE))("RES_FORALL_THM", mk_eq RES_FORALL_DEF),
+       thm (#(FILE), #(LINE))("RES_EXISTS_THM", mk_eq RES_EXISTS_DEF),
+       thm (#(FILE), #(LINE))("RES_EXISTS_UNIQUE_THM",
                                mk_eq RES_EXISTS_UNIQUE_DEF),
-       thm (#(FNAME), #(LINE))("RES_SELECT_THM", mk_eq RES_SELECT_DEF))
+       thm (#(FILE), #(LINE))("RES_SELECT_THM", mk_eq RES_SELECT_DEF))
     end
 
 
@@ -3817,7 +3817,7 @@ val RES_FORALL_TRUE = let
   val timpT_th = List.nth(CONJUNCTS (SPEC xINP_t IMP_CLAUSES), 1)
   val th2 = CONV_RULE (RAND_CONV (QUANT_CONV (K timpT_th))) th1
 in
-  thm (#(FNAME), #(LINE))("RES_FORALL_TRUE", TRANS th2 (SPEC T FORALL_SIMP))
+  thm (#(FILE), #(LINE))("RES_FORALL_TRUE", TRANS th2 (SPEC T FORALL_SIMP))
 end
 
 (* (?x::P. F) = F *)
@@ -3832,7 +3832,7 @@ val RES_EXISTS_FALSE = let
   val tandF_th = List.nth(CONJUNCTS (SPEC xINP_t AND_CLAUSES), 3)
   val th2 = CONV_RULE (RAND_CONV (QUANT_CONV (K tandF_th))) th1
 in
-  thm (#(FNAME), #(LINE))("RES_EXISTS_FALSE", TRANS th2 (SPEC F EXISTS_SIMP))
+  thm (#(FILE), #(LINE))("RES_EXISTS_FALSE", TRANS th2 (SPEC F EXISTS_SIMP))
 end
 
 (*---------------------------------------------------------------------------
@@ -3902,7 +3902,7 @@ val BOOL_FUN_CASES_THM =
      val abcd3 = SPEC fF (GEN x abcd2)
      val abcd  = MP abcd3 (REFL fF)
 in
-   thm (#(FNAME), #(LINE))("BOOL_FUN_CASES_THM", GEN f abcd)
+   thm (#(FILE), #(LINE))("BOOL_FUN_CASES_THM", GEN f abcd)
 end;
 
 (*---------------------------------------------------------------------------
@@ -3961,14 +3961,14 @@ val BOOL_FUN_INDUCT =
      val b4 = imp_and (DISCH (mk_comb(P,KF)) b3)
      val b  = imp_and (DISCH (mk_comb(P,KT)) b4)
 in
-   thm (#(FNAME), #(LINE))("BOOL_FUN_INDUCT", GEN P b)
+   thm (#(FILE), #(LINE))("BOOL_FUN_INDUCT", GEN P b)
 end;
 
 (*---------------------------------------------------------------------------
      literal_case_THM = |- !f x. literal_case f x = f x
  ---------------------------------------------------------------------------*)
 
-val literal_case_THM = thm (#(FNAME), #(LINE))("literal_case_THM",
+val literal_case_THM = thm (#(FILE), #(LINE))("literal_case_THM",
  let val f = “f:'a->'b”
      val x = “x:'a”
  in
@@ -3981,7 +3981,7 @@ val literal_case_THM = thm (#(FNAME), #(LINE))("literal_case_THM",
 (*        |- P (literal_case (\x. N x) M) = (literal_case (\x. P (N x)) M)   *)
 (*---------------------------------------------------------------------------*)
 
-val literal_case_RAND = thm (#(FNAME), #(LINE))("literal_case_RAND",
+val literal_case_RAND = thm (#(FILE), #(LINE))("literal_case_RAND",
  let val tm1 = “\x:'a. P (N x:'b):'c”
      val tm2 = “M:'a”
      val tm3 = “\x:'a. N x:'b”
@@ -3997,7 +3997,7 @@ val literal_case_RAND = thm (#(FNAME), #(LINE))("literal_case_RAND",
 (*         |- (literal_case (\x. N x) M) b = (literal_case (\x. N x b) M)    *)
 (*---------------------------------------------------------------------------*)
 
-val literal_case_RATOR = thm (#(FNAME), #(LINE))("literal_case_RATOR",
+val literal_case_RATOR = thm (#(FILE), #(LINE))("literal_case_RATOR",
  let val M = “M:'a”
      val b = “b:'b”
      val tm1 = “\x:'a. N x:'b->'c”
@@ -4016,7 +4016,7 @@ val literal_case_RATOR = thm (#(FNAME), #(LINE))("literal_case_RATOR",
                    (literal_case f M = literal_case g N)
  ---------------------------------------------------------------------------*)
 
-val literal_case_CONG = thm (#(FNAME), #(LINE))("literal_case_CONG",
+val literal_case_CONG = thm (#(FILE), #(LINE))("literal_case_CONG",
   let val f = mk_var("f",alpha-->beta)
       val g = mk_var("g",alpha-->beta)
       val M = mk_var("M",alpha)
@@ -4044,7 +4044,7 @@ val literal_case_CONG = thm (#(FNAME), #(LINE))("literal_case_CONG",
 (*  |- literal_case (\x. bool_case t u (x=a)) a = t                          *)
 (*---------------------------------------------------------------------------*)
 
-val literal_case_id = thm (#(FNAME), #(LINE))
+val literal_case_id = thm (#(FILE), #(LINE))
 ("literal_case_id",
  let val a = mk_var("a", alpha)
     val x = mk_var("x", alpha)
@@ -4126,7 +4126,7 @@ val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2),
                  paren_style = Always,
                  term_name = GrammarSpecials.core_case_special};
 
-val BOUNDED_THM = thm (#(FNAME), #(LINE))("BOUNDED_THM",
+val BOUNDED_THM = thm (#(FILE), #(LINE))("BOUNDED_THM",
     let val v = “v:bool”
     in
       GEN v (RIGHT_BETA(AP_THM BOUNDED_DEF v))
@@ -4141,7 +4141,7 @@ val BOUNDED_THM = thm (#(FNAME), #(LINE))("BOUNDED_THM",
 (*                    (!x y z. f x (f y z) = f y (f x z))                    *)
 (*---------------------------------------------------------------------------*)
 
-val LCOMM_THM = thm (#(FNAME), #(LINE))("LCOMM_THM",
+val LCOMM_THM = thm (#(FILE), #(LINE))("LCOMM_THM",
  let val x = mk_var("x",alpha)
      val y = mk_var("y",alpha)
      val z = mk_var("z",alpha)
@@ -4159,13 +4159,13 @@ val LCOMM_THM = thm (#(FNAME), #(LINE))("LCOMM_THM",
  end);
 
 
-val DATATYPE_TAG_THM = thm (#(FNAME), #(LINE))("DATATYPE_TAG_THM",
+val DATATYPE_TAG_THM = thm (#(FILE), #(LINE))("DATATYPE_TAG_THM",
     let val x = mk_var("x",alpha)
     in GEN x (RIGHT_BETA (AP_THM DATATYPE_TAG_DEF x))
     end);
 
 
-val DATATYPE_BOOL = thm (#(FNAME), #(LINE))("DATATYPE_BOOL",
+val DATATYPE_BOOL = thm (#(FILE), #(LINE))("DATATYPE_BOOL",
  let val thm1 = INST_TYPE [alpha |-> bool] DATATYPE_TAG_THM
      val bvar = mk_var("bool",bool--> bool-->bool)
  in
@@ -4213,7 +4213,7 @@ val ITSELF_UNIQUE = let
       GEN_ALL (MP (SPECL [“i:'a itself”, “bool$the_value”] typedef_11)
                   allreps_repthevalue)
 in
-  thm (#(FNAME), #(LINE))("ITSELF_UNIQUE",
+  thm (#(FILE), #(LINE))("ITSELF_UNIQUE",
            CHOOSE (“rep:'a itself -> 'a”, ITSELF_TYPE_DEF) all_eq_thevalue)
 end
 
@@ -4231,7 +4231,7 @@ val ITSELF_EQN_RWT = let
   val l2r = SPEC x ITSELF_UNIQUE |> AP_TERM f |> C TRANS (ASSUME l) |> GEN x
                  |> DISCH l
 in
-  thm (#(FNAME), #(LINE))(
+  thm (#(FILE), #(LINE))(
     "ITSELF_EQN_RWT",
     GENL [f,e] $ IMP_ANTISYM_RULE l2r r2l
   )
@@ -4246,7 +4246,7 @@ val itself_Axiom = let
   val fn_exists = EXISTS (“?f:'a itself -> 'b. f (:'a) = e”, witness)
                   fn_behaves
 in
-  thm (#(FNAME), #(LINE))("itself_Axiom", GEN_ALL fn_exists)
+  thm (#(FILE), #(LINE))("itself_Axiom", GEN_ALL fn_exists)
 end
 
 (* prove induction *)
@@ -4256,7 +4256,7 @@ val itself_induction = let
       EQ_MP (SYM (AP_TERM “P:'a itself -> bool” (SPEC_ALL ITSELF_UNIQUE)))
             pval
 in
-  thm (#(FNAME), #(LINE))("itself_induction", GEN_ALL (DISCH_ALL (GEN_ALL pi)))
+  thm (#(FILE), #(LINE))("itself_induction", GEN_ALL (DISCH_ALL (GEN_ALL pi)))
 end
 
 (* define case operator *)
@@ -4270,7 +4270,7 @@ in
     constnames = ["itself_case"],
     witness = EXISTS (“?f:'a itself -> 'b -> 'b. !b. f (:'a) b = b”, witness)
                      (GEN_ALL witness_applied2),
-    loc = mkloc(#(FNAME), #(LINE)-5)
+    loc = mkloc(#(FILE), #(LINE)-5)
   }
 end
 val _ = overload_on("case", “itself_case”)
@@ -4295,8 +4295,8 @@ local
                     (EQ_MP (SYM unique) (ASSUME Px)) |> DISCH_ALL
   val imp2 = EXISTS(mk_exists(x,Px),itself) (ASSUME Pitself) |> DISCH_ALL
 in
-  val FORALL_itself = thm (#(FNAME), #(LINE))("FORALL_itself", fa)
-  val EXISTS_itself = thm (#(FNAME), #(LINE))
+  val FORALL_itself = thm (#(FILE), #(LINE))("FORALL_itself", fa)
+  val EXISTS_itself = thm (#(FILE), #(LINE))
                           ("EXISTS_itself", IMP_ANTISYM_RULE imp1 imp2)
 end;
 
@@ -4314,9 +4314,9 @@ local
   val PULL_FORALL2 = LEFT_AND_FORALL_THM |> SPEC_ALL
   val PULL_FORALL3 = RIGHT_AND_FORALL_THM |> SPEC_ALL |> flip
 in
-  val PULL_EXISTS = thm (#(FNAME), #(LINE))("PULL_EXISTS",
+  val PULL_EXISTS = thm (#(FILE), #(LINE))("PULL_EXISTS",
     LIST_CONJ [PULL_EXISTS1, PULL_EXISTS2, PULL_EXISTS3] |> GENL [Pab, Qb])
-  val PULL_FORALL = thm (#(FNAME), #(LINE))("PULL_FORALL",
+  val PULL_FORALL = thm (#(FILE), #(LINE))("PULL_FORALL",
     LIST_CONJ [PULL_FORALL1, PULL_FORALL2, PULL_FORALL3] |> GENL [Pab, Qb])
 end
 
@@ -4324,7 +4324,7 @@ end
 (* PEIRCE  =  |- ((P ==> Q) ==> P) ==> P                                     *)
 (*---------------------------------------------------------------------------*)
 
-val PEIRCE = thm (#(FNAME), #(LINE))
+val PEIRCE = thm (#(FILE), #(LINE))
 ("PEIRCE",
  let val th1 = ASSUME “(P ==> Q) ==> P”
      val th2 = ASSUME “P:bool”
@@ -4358,7 +4358,7 @@ val JRH_INDUCT_UTIL = let
   val P_eta = SPEC P (INST_TYPE [beta |-> bool] ETA_AX)
   val ExP_eta = AP_TERM “(?) : ('a -> bool) -> bool” P_eta
 in
-  thm (#(FNAME), #(LINE))("JRH_INDUCT_UTIL",
+  thm (#(FILE), #(LINE))("JRH_INDUCT_UTIL",
                           GENL [P, t] (DISCH asm_t (EQ_MP ExP_eta ExPx)))
 end
 
@@ -4386,7 +4386,7 @@ val _ = add_user_printer ("bool.LET", “LET f x”)
 val _ = add_absyn_postprocessor "bool.LET"
 
 (* |- |- !A B. A \/ B <=> ~A ==> B *)
-val DISJ_EQ_IMP = thm (#(FNAME), #(LINE))("DISJ_EQ_IMP",
+val DISJ_EQ_IMP = thm (#(FILE), #(LINE))("DISJ_EQ_IMP",
   let
     val lemma = NOT_CLAUSES |> CONJUNCT1 |> SPEC ``A:bool``
   in
@@ -4404,7 +4404,7 @@ val DISJ_EQ_IMP = thm (#(FNAME), #(LINE))("DISJ_EQ_IMP",
 (* (HOL-Light compatible)                                                    *)
 (* ------------------------------------------------------------------------- *)
 
-val CONTRAPOS_THM = thm (#(FNAME), #(LINE)) ("CONTRAPOS_THM",
+val CONTRAPOS_THM = thm (#(FILE), #(LINE)) ("CONTRAPOS_THM",
     MONO_NOT_EQ |> SYM
                 |> INST [“x:bool” |-> “t1:bool”, “y:bool” |-> “t2:bool”]
                 |> GENL [“t1:bool”, “t2:bool”]);
diff --git a/src/combin/combinScript.sml b/src/combin/combinScript.sml
index 7364fe7c9d..a829a8752b 100644
--- a/src/combin/combinScript.sml
+++ b/src/combin/combinScript.sml
@@ -20,16 +20,16 @@ val _ = new_theory "combin";
 
 fun def (s,l) p = Q.new_definition_at (DB_dtype.mkloc(s,l,false)) p
 
-val K_DEF = def(#(FNAME),#(LINE))("K_DEF",        `K = \x y. x`);
-val S_DEF = def(#(FNAME),#(LINE))("S_DEF",        `S = \f g x. f x (g x)`);
-val I_DEF = def(#(FNAME),#(LINE))("I_DEF",        `I = S K (K:'a->'a->'a)`);
-val C_DEF = def(#(FNAME),#(LINE))("C_DEF",        `C = \f x y. f y x`);
-val W_DEF = def(#(FNAME),#(LINE))("W_DEF",        `W = \f x. f x x`);
-val o_DEF = def(#(FNAME),#(LINE))("o_DEF", `$o f g = \x. f(g x)`);
+val K_DEF = def(#(FILE),#(LINE))("K_DEF",        `K = \x y. x`);
+val S_DEF = def(#(FILE),#(LINE))("S_DEF",        `S = \f g x. f x (g x)`);
+val I_DEF = def(#(FILE),#(LINE))("I_DEF",        `I = S K (K:'a->'a->'a)`);
+val C_DEF = def(#(FILE),#(LINE))("C_DEF",        `C = \f x y. f y x`);
+val W_DEF = def(#(FILE),#(LINE))("W_DEF",        `W = \f x. f x x`);
+val o_DEF = def(#(FILE),#(LINE))("o_DEF", `$o f g = \x. f(g x)`);
 val _ = set_fixity "o" (Infixr 800)
-val APP_DEF = def(#(FNAME),#(LINE)) ("APP_DEF",   `$:> x f = f x`);
+val APP_DEF = def(#(FILE),#(LINE)) ("APP_DEF",   `$:> x f = f x`);
 
-val UPDATE_def = def(#(FNAME),#(LINE))("UPDATE_def",
+val UPDATE_def = def(#(FILE),#(LINE))("UPDATE_def",
    `UPDATE a b = \f c. if a = c then b else f c`);
 
 val _ = set_fixity ":>" (Infixl 310);
diff --git a/src/probability/borelScript.sml b/src/probability/borelScript.sml
index dc64287159..733e0d0368 100644
--- a/src/probability/borelScript.sml
+++ b/src/probability/borelScript.sml
@@ -8120,8 +8120,8 @@ Theorem IN_MEASURABLE_BOREL_POW_EXP:
         (!x. x IN space a ==> h x = (f x) pow (g x)) ==> h IN Borel_measurable a
 Proof
     rw[] >> simp[Once IN_MEASURABLE_BOREL_PLUS_MINUS] >>
-    ‘!P. {x | P (g x)} INTER space a IN subsets a` by (rw[] >>
-        `{x | P (g x)} INTER space a = BIGUNION {{x | g x = n} INTER space a | P n}’ by (
+    ‘!P. {x | P (g x)} INTER space a IN subsets a’ by (rw[] >>
+        ‘{x | P (g x)} INTER space a = BIGUNION {{x | g x = n} INTER space a | P n}’ by (
             rw[Once EXTENSION,IN_BIGUNION] >> eq_tac >> strip_tac >> gvs[] >>
             qexists_tac ‘{y | g y = g x} INTER space a’ >> simp[] >> qexists_tac ‘g x’ >> simp[]) >>
         pop_assum SUBST1_TAC >> irule SIGMA_ALGEBRA_COUNTABLE_UNION >>
@@ -8130,11 +8130,11 @@ Proof
     map_every (fn (pos,tm,qex,ths) => irule_at pos tm >> qexistsl_tac qex >> simp ths) [
         (Pos hd,IN_MEASURABLE_BOREL_ADD',[‘λx. fn_minus f x pow g x * indicator_fn {x | EVEN (g x)} x’,
             ‘λx. fn_plus f x pow g x * indicator_fn {x | $< 0 (g x)} x’],[]),
-        (Pos (el 2),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | EVEN (g x)}`,`λx. fn_minus f x pow g x’],[]),
+        (Pos (el 2),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | EVEN (g x)}’,‘λx. fn_minus f x pow g x’],[]),
         (Pos (el 2),IN_MEASURABLE_BOREL_INDICATOR,[‘{x | EVEN (g x)} INTER space a’],[]),
-        (Pos (el 3),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | $< 0 (g x)}`,`λx. fn_plus f x pow g x’],[]),
+        (Pos (el 3),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | $< 0 (g x)}’,‘λx. fn_plus f x pow g x’],[]),
         (Pos (el 2),IN_MEASURABLE_BOREL_INDICATOR,[‘{x | $< 0 (g x)} INTER space a’],[]),
-        (Pos last,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | ODD (g x)}`,`λx. fn_minus f x pow g x’],[]),
+        (Pos last,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | ODD (g x)}’,‘λx. fn_minus f x pow g x’],[]),
         (Pos (el 2),IN_MEASURABLE_BOREL_INDICATOR,[‘{x | ODD (g x)} INTER space a’],[])] >>
     pop_assum kall_tac >>
     ‘!pf. pf IN Borel_measurable a /\ (!x. 0 <= pf x) ==> (λx. pf x pow g x) IN Borel_measurable a’ by (
@@ -8142,7 +8142,7 @@ Proof
         qexistsl_tac [‘λn x. pf x pow n * indicator_fn {x | g x = n} x’] >> simp[pow_pos_le,INDICATOR_FN_POS,le_mul] >>
         simp[RIGHT_AND_FORALL_THM] >> strip_tac >>
         map_every (fn (pos,tm,qex,ths) => irule_at pos tm >> simp[] >> qexistsl_tac qex >> simp ths) [
-            (Any,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | g x = n}`,`λx. pf x pow n’],[]),
+            (Any,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | g x = n}’,‘λx. pf x pow n’],[]),
             (Pos hd,IN_MEASURABLE_BOREL_POW',[‘n’,‘pf’],[]),
             (Pos hd,IN_MEASURABLE_BOREL_INDICATOR,[‘{x | g x = n} INTER space a’],[indicator_fn_def])] >>
         rw[] >> qspecl_then [‘g x’,‘pf x pow g x’] mp_tac ext_suminf_sing_general >>
diff --git a/src/tactictoe/examples/ttt_demoScript.sml b/src/tactictoe/examples/ttt_demoScript.sml
index 623e78ef74..b9fc943a78 100644
--- a/src/tactictoe/examples/ttt_demoScript.sml
+++ b/src/tactictoe/examples/ttt_demoScript.sml
@@ -31,7 +31,7 @@ open listTheory
 (* ttt ([],``(!n. f n = c) ==> (MAP f ls = REPLICATE (LENGTH ls) c)``); *)
 val ex2 = store_thm("ex2",
   ``(!n. f n = c) ==> (MAP f ls = REPLICATE (LENGTH ls) c)``,
-  asm_simp_tac (srw_ss () ++ boolSimps.LET_ss ++ ARITH_ss)) [LIST_EQ_REWRITE] >>
+  asm_simp_tac (srw_ss () ++ boolSimps.LET_ss ++ ARITH_ss) [LIST_EQ_REWRITE] >>
   metis_tac [EL_MAP, rich_listTheory.EL_REPLICATE]
   );
 
diff --git a/src/tactictoe/src/tttToken.sml b/src/tactictoe/src/tttToken.sml
index 281a4cf55d..dcb57a7bac 100644
--- a/src/tactictoe/src/tttToken.sml
+++ b/src/tactictoe/src/tttToken.sml
@@ -175,7 +175,7 @@ fun inst_term sterm stac =
 (*
 load "tttToken"; open tttToken;
 val stac = "EXISTS_TAC ``1:num``";
-val stac' = QFRead.fromString false stac;
+val stac' = HolParser.fromString false stac;
 val (astac,sterm) = valOf (abstract_term stac');
 val istac = inst_term "2:num" astac;
 *)
diff --git a/src/tactictoe/src/tttUnfold.sml b/src/tactictoe/src/tttUnfold.sml
index 0807d55fdd..2f03de6947 100644
--- a/src/tactictoe/src/tttUnfold.sml
+++ b/src/tactictoe/src/tttUnfold.sml
@@ -973,7 +973,7 @@ fun rm_spaces s =
 
 fun sketch_wrap thy file =
   let
-    val s1 = QFRead.inputFile file
+    val s1 = HolParser.inputFile file
     val s2 = rm_spaces (rm_comment s1)
     val sl = partial_sml_lexer s2
     val lexdir =  tactictoe_dir ^ "/log/lexer"
diff --git a/tools-poly/configure.sml b/tools-poly/configure.sml
index f4ea305ba2..669828023f 100644
--- a/tools-poly/configure.sml
+++ b/tools-poly/configure.sml
@@ -425,13 +425,14 @@ val _ = work_in_dir
 val _ = work_in_dir
           "Holmake" (fullPath [HOLDIR, "tools", "Holmake", "poly"])
           (fn () => (OS.FileSys.chDir "..";
-                     systeml [lexer, "QuoteFilter"] ;
+                     systeml [lexer, "HolLex"];
+                     systeml [lexer, "QuoteFilter"];
                      OS.FileSys.chDir "poly";
                      polyc_compile (SOME "../mlton/Holmake.mlb")
                                    "poly-Holmake.ML" hmakebin))
 
 (* unquote - the quotation filter *)
-val _ = work_in_dir "unquote." qfdir
+val _ = work_in_dir "unquote" qfdir
                     (fn () => (polyc_compile NONE "poly-unquote.ML" qfbin))
 
 (* holdeptool *)
diff --git a/tools-poly/holrepl.ML b/tools-poly/holrepl.ML
index bc2aca0308..527d939325 100644
--- a/tools-poly/holrepl.ML
+++ b/tools-poly/holrepl.ML
@@ -163,7 +163,7 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm,
         in fn () =>
           let
             (* Create a new lexer for each command block. *)
-            val {read, ...} = QFRead.inputToReader true "" input;
+            val {read, ...} = HolParser.inputToReader true "" input;
             val endOfBlock = ref false;
             fun read' () = case read () of
                 NONE => (endOfBlock := true; NONE)
@@ -195,7 +195,7 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm,
           fun cgen() = !cgenref()
           fun bind_cgen () =
               let
-                val {read, ...} = QFRead.streamToReader true "" TextIO.stdIn
+                val {read, ...} = HolParser.streamToReader true "" TextIO.stdIn
               in
                 cgenref := read
               end
diff --git a/tools-poly/poly-build.ML b/tools-poly/poly-build.ML
index 82c40a2492..0720da6bea 100644
--- a/tools-poly/poly-build.ML
+++ b/tools-poly/poly-build.ML
@@ -17,8 +17,8 @@ val _ = useC "HOLFileSys";
 val _ = useC "Holdep_tokens";
 val _ = useC "HM_SimpleBuffer";
 val _ = useC "AttributeSyntax";
-val _ = use "../tools/Holmake/QuoteFilter.sml";
-val _ = useC "QFRead";
+val _ = use "../tools/Holmake/HolLex.sml";
+val _ = useC "HolParser";
 val _ = useC "Holdep";
 val _ = use "../tools/Holmake/Holmake_tools_dtype.sml";
 val _ = use "../tools/Holmake/terminal_primitives.sig";
diff --git a/tools-poly/poly/poly-init2.ML b/tools-poly/poly/poly-init2.ML
index a02d0ee20d..bfc00fd177 100644
--- a/tools-poly/poly/poly-init2.ML
+++ b/tools-poly/poly/poly-init2.ML
@@ -6,6 +6,7 @@ val _ = use "Holmake/Systeml.sml"
 
 val _ = use "../tools/Holmake/AttributeSyntax.sig";
 val _ = use "../tools/Holmake/AttributeSyntax.sml";
+val _ = use "../tools/Holmake/HolLex.sml";
 val _ = use "../tools/Holmake/QuoteFilter.sml";
 val _ = use "../tools/Holmake/HM_SimpleBuffer.sig";
 val _ = use "../tools/Holmake/HM_SimpleBuffer.sml";
@@ -17,6 +18,8 @@ val _ = use "../tools/Holmake/HOLFileSys.sig";
 val _ = use "../tools/Holmake/HOLFileSys.sml";
 val _ = use "../tools/Holmake/QFRead.sig";
 val _ = use "../tools/Holmake/QFRead.sml";
+val _ = use "../tools/Holmake/HolParser.sig";
+val _ = use "../tools/Holmake/HolParser.sml";
 val _ = use "poly/quse.sig";
 val _ = use "poly/quse.sml";
 
diff --git a/tools-poly/poly/quse.sml b/tools-poly/poly/quse.sml
index 326f8e0ae8..297ca961b9 100644
--- a/tools-poly/poly/quse.sml
+++ b/tools-poly/poly/quse.sml
@@ -1,7 +1,7 @@
 structure QUse :> QUse =
 struct
 
-fun use_reader fname (reader as {read = infn0, eof, reset}) =
+fun use_reader fname (reader as {read = infn0, eof}) =
   let
     val lineNo = ref 1
     fun infn () =
@@ -17,12 +17,12 @@ fun use_reader fname (reader as {read = infn0, eof, reset}) =
                            Compiler.CPLineNo (fn () => !lineNo)]) ()
   end
 
-fun use fname = use_reader fname (QFRead.fileToReader fname)
+fun use fname = use_reader fname (HolParser.fileToReader fname)
 
 fun useScript fname =
     let
       val istream = TextIO.openIn fname
-      val reader = QFRead.streamToReader true fname istream
+      val reader = HolParser.streamToReader true fname istream
       val _ = use_reader fname reader
               handle e => (TextIO.closeIn istream; raise e)
     in
diff --git a/tools/Holmake/.gitignore b/tools/Holmake/.gitignore
index 28bd1009d3..e2010ab40a 100644
--- a/tools/Holmake/.gitignore
+++ b/tools/Holmake/.gitignore
@@ -1 +1,2 @@
 QuoteFilter.sml
+HolLex.sml
diff --git a/tools/Holmake/AttributeSyntax.sig b/tools/Holmake/AttributeSyntax.sig
index d54da729e0..9c6bb6bd04 100644
--- a/tools/Holmake/AttributeSyntax.sig
+++ b/tools/Holmake/AttributeSyntax.sig
@@ -2,6 +2,7 @@ signature AttributeSyntax =
 sig
 
   val mk_strsafe : string -> string
+  val bslash_escape : char -> string
   val bslash_escape_s : string -> string
   val dest_ml_thm_binding : string -> {keyword: string, name : string,
                                        name_attr_original : string,
diff --git a/tools/Holmake/HolLex b/tools/Holmake/HolLex
new file mode 100644
index 0000000000..9235010454
--- /dev/null
+++ b/tools/Holmake/HolLex
@@ -0,0 +1,418 @@
+(* this is an -*- sml -*- file, or near enough *)
+fun inc r = (r := !r + 1)
+fun dec r = (r := !r - 1)
+
+datatype decl
+  = DefinitionDecl of {
+      head: int * string, quote: qbody, termination: {tok: int, decls: decls} option,
+      end_tok: int option, stop: int}
+  | DatatypeDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int}
+  | QuoteDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int}
+  | QuoteEqnDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int}
+  | InductiveDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int}
+  | BeginType of int * string
+  | BeginSimpleThm of int * string
+  | TheoremDecl of {
+      head: int * string, quote: qbody, proof_tok: (int * string) option,
+      body: decls, qed: int option, stop: int}
+  | Chunk of int
+  | Semi of int
+  | FullQuote of {
+      head: int * string, type_q: int option,
+      quote: qbody, end_tok: (int * string) option, stop: int}
+  | Quote of {head: int * string, quote: qbody, end_tok: (int * string) option, stop: int}
+  | String of int * int
+  | LinePragma of int
+  | LinePragmaWith of int * string
+  | FilePragma of int
+  | FilePragmaWith of int * string
+
+and decls = Decls of {start: int, decls: decl list, stop: int}
+
+and antiq
+  = Ident of int * string
+  | Paren of {start_tok: int, decls: decls, end_tok: int option, stop: int}
+  | BadAntiq of int
+
+and qdecl
+  = QuoteAntiq of int * antiq
+  | DefinitionLabel of int * string
+  | QuoteComment of int * int
+
+and qbody = QBody of {start: int, toks: qdecl list, stop: int}
+
+datatype token
+  = Decl of decl * token option (* from INITIAL *)
+  | CloseParen of int (* from INITIAL *)
+  | QED of int (* from INITIAL *)
+  | EndTok of int (* from INITIAL, quote, holcomment *)
+  | Comment (* from comment *)
+  | Antiq of antiq * token option (* from ANTIQ *)
+  | StringEnd of int (* from string *)
+  | HolStrLitEnd of int * string (* from holstrlit *)
+  | ProofLine of int * string (* from quote, holcomment *)
+  | TerminationTok of int (* from quote, holcomment *)
+  | QuoteEnd of int * string (* from quote, holcomment *)
+  | FullQuoteEnd of int * string (* from quote, holcomment *)
+  | QDecl of qdecl * token option (* from quote *)
+  | EOF of int (* from every state *)
+
+type lexresult = token
+
+datatype state = STATE of {
+  parseError: int * int -> string -> unit,
+  pardepth: int ref,
+  comdepth: int ref,
+  comstart: (int * int) option ref
+}
+
+fun noDecls pos = Decls {start = pos, decls = [], stop = pos}
+
+exception Unreachable
+datatype 'a test_result = TestOk of 'a | TestBad | TestSkip
+
+fun forceCloseComment (STATE {parseError, comdepth, comstart, ...}) stop buf =
+  case !comstart of
+    SOME pos => (
+    parseError pos "unterminated comment";
+    comdepth := 0; comstart := NONE;
+    QuoteComment (#1 pos, stop) :: buf)
+  | _ => buf
+
+fun parseQuoteBody (arg as STATE {parseError, ...}) continue pos test = let
+  fun go buf lookahead = let
+    val tk = case lookahead of SOME tk => tk | NONE => continue()
+    fun finish stop =
+      QBody {start = #2 pos, toks = rev (forceCloseComment arg stop buf), stop = stop}
+    fun cont (p, t) strong =
+      case test tk of
+        TestBad =>
+        if strong then (parseError pos "unterminated quote"; (finish p, NONE, p, SOME tk))
+        else (parseError (p, p + size t) ("unexpected '"^t^"'"); go buf NONE)
+      | TestSkip => go buf NONE
+      | TestOk out => (finish p, SOME out, p + size t, NONE)
+    in case tk of
+        QDecl (qd, extra) => go (qd :: buf) extra
+      | QuoteEnd pt => cont pt false
+      | FullQuoteEnd pt => cont pt false
+      | ProofLine pt => cont pt true
+      | TerminationTok p => cont (p, "Termination") true
+      | EndTok p => cont (p, "End") true
+      | EOF p => (parseError pos "unterminated quote"; (finish p, NONE, p, SOME tk))
+      | _ => raise Unreachable
+    end
+  in go [] NONE end
+
+fun parseDecls (STATE {parseError, pardepth, ...}) continue pos test = let
+  fun go buf lookahead = let
+    val tk = case lookahead of SOME tk => tk | NONE => continue()
+    fun finish stop = Decls {start = pos, decls = rev buf, stop = stop}
+    fun cont (p, t) strong =
+      case test tk of
+        NONE =>
+        if strong then (finish p, NONE, p, SOME tk)
+        else (parseError (p, p + size t) ("unexpected '"^t^"'"); go buf NONE)
+      | out => (finish p, out, p + size t, NONE)
+    in case tk of
+        Decl (tk, look) => go (tk :: buf) look
+      | CloseParen p => cont (p, ")") false
+      | EndTok p => cont (p, "End") true
+      | QED p => cont (p, "QED") true
+      | EOF p => (finish p, NONE, p, SOME tk)
+      | _ => raise Unreachable
+    end
+  val n = !pardepth
+  in pardepth := 0; go [] NONE before pardepth := n end
+
+fun fullQuoteMatch "``" "``" = true
+  | fullQuoteMatch "\226\128\156" "\226\128\157" = true
+  | fullQuoteMatch _ _ = false
+
+fun quoteMatch "`" "`" = true
+  | quoteMatch "\226\128\152" "\226\128\153" = true
+  | quoteMatch _ _ = false
+
+fun strlitMatch "\"" "\"" = true
+  | strlitMatch "\226\128\185" "\226\128\186" = true
+  | strlitMatch "\194\171" "\194\187" = true
+  | strlitMatch _ _ = false
+
+fun parseQuoteEndDef yyarg continue pos text mk = let
+  val (q, end_tok, stop, extra) = parseQuoteBody yyarg continue (pos, pos + size text) (fn
+      EndTok p => TestOk p
+    | QuoteEnd _ => TestSkip
+    | FullQuoteEnd _ => TestSkip
+    | _ => TestBad)
+  in
+    Decl (mk {head = (pos, text), quote = q, end_tok = end_tok, stop = stop}, extra)
+  end
+
+fun parseFullQuote (yyarg as STATE {parseError, ...}) continue pos yytext type_q = let
+  val qlen = if String.sub(yytext,0) = #"`" then 2 else 3
+  val text = String.substring (yytext, 0, qlen)
+  val (q, end_tok, stop, extra) = parseQuoteBody yyarg continue (pos, pos + qlen) (fn
+      FullQuoteEnd (tk as (p, t)) => (
+        if fullQuoteMatch text t then () else parseError (p, p + size t) ("unexpected '"^t^"'");
+        TestOk tk)
+    | QuoteEnd _ => TestSkip
+    | _ => TestBad)
+  in
+    Decl (FullQuote {head = (pos, text), type_q = type_q,
+      quote = q, end_tok = end_tok, stop = stop}, extra)
+  end
+
+fun parseQuote (yyarg as STATE {parseError, ...}) continue pos yytext = let
+  val qlen = if String.sub(yytext,0) = #"`" then 1 else 3
+  val text = String.substring (yytext, 0, qlen)
+  val (q, end_tok, stop, extra) = parseQuoteBody yyarg continue (pos, pos + qlen) (fn
+      QuoteEnd (tk as (p, t)) => (
+        if quoteMatch text t then () else parseError (p, p + size t) ("unexpected '"^t^"'");
+        TestOk tk)
+    | FullQuoteEnd _ => TestSkip
+    | _ => TestBad)
+  in
+    Decl (Quote {head = (pos, text), quote = q, end_tok = end_tok, stop = stop}, extra)
+  end
+
+fun eof (_:state) = EOF
+
+%%
+%structure HolLex
+%s string stringlbrk comment holcomment quote holstrlit holstrlitlbrk ANTIQ;
+%arg (UserDeclarations.STATE {pardepth, comdepth, comstart, parseError});
+%full
+%posarg
+%eofpos
+
+letter = [A-Za-z];
+digit = [0-9];
+nonspecial_symbol = [-!%&$+/<>?@~|#*\\^];
+symbol = {nonspecial_symbol} | [=:];
+symbolident = ":" {symbol}+ | "=" {symbol}+ | {nonspecial_symbol} {symbol}*;
+alphaMLid_tailchar = ({letter} | {digit} | _ | "'");
+alphaMLid = {letter} {alphaMLid_tailchar}*;
+alphaMLid_list = {alphaMLid} (","{alphaMLid})*;
+quotedsymbolid = "\"" [^\034]+ "\"";
+ws = [\ \t];
+newline = "\n" | "\013\n";
+optallws = ({ws}|{newline})*;
+forcedallws = ({ws}|{newline})+;
+attributeValue_tailchar = {alphaMLid_tailchar} | ".";
+attributeValue = {letter} {attributeValue_tailchar}*;
+attributeEqnRHS = {attributeValue}({forcedallws}{attributeValue})*;
+defn_attribute =
+  {alphaMLid}{optallws} ("="{optallws}{attributeEqnRHS}{optallws})?;
+defn_attribute_list = {defn_attribute} (","({ws}|{newline})*{defn_attribute})*;
+MLid =  {alphaMLid} | {symbolident};
+QUALMLid = {MLid} ("." {MLid})*;
+QUALalphaMLid = {alphaMLid} ("." {alphaMLid})*;
+locpragma = "(*#loc" {ws}+ {digit}* {ws}+ {digit}* {ws}* "*)";
+lowergreek = "\206" [\177-\191] | "\207" [\128-\137];
+fullquotebegin = "``" | "\226\128\156";
+fullquoteend = "``" | "\226\128\157";
+quotebegin = "`" | "\226\128\152";
+quoteend = "`" | "\226\128\153";
+Theorempfx = ("Theorem"|"Triviality"){ws}+{alphaMLid}({ws}*"["{alphaMLid_list}"]")?;
+Quote_eqnpfx = "Quote"{ws}+{alphaMLid}{ws}*"="{ws}*{QUALalphaMLid}{ws}*":";
+Quote_pfx = "Quote"{ws}+{QUALalphaMLid}{ws}*":";
+HOLconjunction = "/\092" | "\226\136\167";
+DefinitionLabelID = {letter}{alphaMLid_tailchar}* | "~"{alphaMLid_tailchar}+ | {HOLconjunction};
+DefinitionLabel = "["{ws}*{DefinitionLabelID}?("["{alphaMLid_list}"]")?{ws}*":"?{ws}*"]";
+Definitionpfx = "Definition"{ws}+{alphaMLid}({ws}*"["{optallws}{defn_attribute_list}"]")?{ws}*":";
+declforms = "val"|"fun"|"structure"|"signature"|"functor"|"abstype"|"datatype"|"exception"|"open"|"infix"[lr]?|"local";
+Inductivepfx = ("Co")?"Inductive"{ws}+{alphaMLid}{ws}*":";
+HOLSTRLITstart = "\"" | "\226\128\185" | "\194\171";
+HOLSTRLITend = "\"" | "\226\128\186" | "\194\187";
+ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]")?;
+%%
+
+<INITIAL>"(*" => (
+  comdepth := 1; YYBEGIN comment;
+  case continue() of
+    Comment => (YYBEGIN INITIAL; continue())
+  | EOF p => (parseError (yypos, yyend) "unterminated comment"; EOF p)
+  | _ => raise Unreachable
+);
+<INITIAL>"(" => (inc pardepth; continue());
+<INITIAL>")" => (if !pardepth < 1 then CloseParen yypos else (dec pardepth; continue()));
+<INITIAL>^"Datatype"{ws}*":" => (
+  YYBEGIN quote;
+  parseQuoteEndDef yyarg continue yypos yytext DatatypeDecl before YYBEGIN INITIAL
+);
+<INITIAL>^("Type"|"Overload"){ws}+({alphaMLid}|{quotedsymbolid})("["{alphaMLid_list}"]")?{ws}*"=" =>
+  (Decl (BeginType (yypos, yytext), NONE));
+<INITIAL>{Theorempfx}{ws}*":" => (let
+  val _ = YYBEGIN quote
+  val (q, proof_tok, stop, extra) =
+    parseQuoteBody yyarg continue (yypos, yyend) (fn
+        ProofLine l => TestOk l
+      | QuoteEnd _ => TestSkip
+      | FullQuoteEnd _ => TestSkip
+      | _ => TestBad)
+  val _ = YYBEGIN INITIAL
+  val (decls, qed, stop, extra) =
+    case extra of
+      SOME (QED p) => (noDecls stop, SOME p, p + 3, NONE)
+    | SOME _ => (noDecls stop, NONE, stop, extra)
+    | NONE => parseDecls yyarg continue stop (fn QED p => SOME p | _ => NONE)
+  in
+    Decl (TheoremDecl {
+      head = (yypos, yytext), quote = q, proof_tok = proof_tok,
+      body = decls, qed = qed, stop = stop}, extra)
+  end);
+<INITIAL>^"QED" => (QED yypos);
+<INITIAL>^{Definitionpfx} => (let
+  val _ = YYBEGIN quote
+  val (q, tok, stop, extra) = parseQuoteBody yyarg continue (yypos, yypos + size yytext) (fn
+      TerminationTok p => TestOk (p, true)
+    | EndTok p => TestOk (p, false)
+    | QuoteEnd _ => TestSkip
+    | FullQuoteEnd _ => TestSkip
+    | _ => TestBad)
+  val _ = YYBEGIN INITIAL
+  val (termination, end_tok, stop, extra) =
+    case (tok, extra) of
+      (SOME (p, true), NONE) => let
+      val (decls, end_tok, stop, extra) = parseDecls yyarg continue stop
+        (fn EndTok p => SOME p | _ => NONE)
+      in (SOME {tok = p, decls = decls}, end_tok, stop, extra) end
+    | (SOME (p, false), NONE) => (NONE, SOME p, stop, NONE)
+    | _ => (NONE, NONE, stop, extra)
+  in
+    Decl (DefinitionDecl {
+      head = (yypos, yytext), quote = q,
+      termination = termination, end_tok = end_tok, stop = stop}, extra)
+  end);
+<INITIAL>^{Quote_pfx} => (
+  YYBEGIN quote;
+  parseQuoteEndDef yyarg continue yypos yytext QuoteDecl before YYBEGIN INITIAL
+);
+<INITIAL>^{Quote_eqnpfx} => (
+  YYBEGIN quote;
+  parseQuoteEndDef yyarg continue yypos yytext QuoteEqnDecl before YYBEGIN INITIAL
+);
+<INITIAL>{Theorempfx}({ws}|{newline})+"=" => (Decl (BeginSimpleThm (yypos, yytext), NONE));
+<INITIAL>^{Inductivepfx} => (
+  YYBEGIN quote;
+  parseQuoteEndDef yyarg continue yypos yytext InductiveDecl before YYBEGIN INITIAL
+);
+<INITIAL>{fullquotebegin} {ws}* ":" ({letter} | {ws} | [('] | {digit} | {lowergreek}) => (
+  YYBEGIN quote;
+  yybufpos := !yybufpos - 1; (* unread last character *)
+  parseFullQuote yyarg continue yypos yytext (SOME (yyend - 2)) before YYBEGIN INITIAL
+);
+<INITIAL>{fullquotebegin} {ws}* ":" {newline} => (let
+  val _ = YYBEGIN quote
+  val nllen = if String.sub(yytext, size yytext-2) = #":" then 1 else 2
+  val _ = yybufpos := !yybufpos - nllen; (* unread newline *)
+  in parseFullQuote yyarg continue yypos yytext (SOME (yyend - nllen - 1)) before YYBEGIN INITIAL end);
+<INITIAL>{fullquotebegin} {ws}* ":^" => (
+  YYBEGIN quote;
+  yybufpos := !yybufpos - 1; (* unread last character *)
+  parseFullQuote yyarg continue yypos yytext (SOME (yyend - 2)) before YYBEGIN INITIAL
+);
+<INITIAL>{fullquotebegin} => (
+  YYBEGIN quote;
+  parseFullQuote yyarg continue yypos yytext NONE before YYBEGIN INITIAL
+);
+<INITIAL>{quotebegin} => (
+  YYBEGIN quote;
+  parseQuote yyarg continue yypos yytext before YYBEGIN INITIAL
+);
+<INITIAL>"#(LINE)" => (Decl (LinePragma yypos, NONE));
+<INITIAL>"#(LINE="[0-9]+")" => (Decl (LinePragmaWith (yypos, yytext), NONE));
+<INITIAL>"#(FILE)" => (Decl (FilePragma yypos, NONE));
+<INITIAL>"#(FILE="[-A-Za-z0-9/$()_.]+")" => (Decl (FilePragmaWith (yypos, yytext), NONE));
+<INITIAL>"\"" => (
+  YYBEGIN string;
+  case continue() of
+    StringEnd p => (YYBEGIN INITIAL; Decl (String (yypos, p), NONE))
+  | tk as EOF p => (
+    parseError (yypos, yyend) "unterminated string";
+    YYBEGIN INITIAL; Decl (String (yypos, p), SOME tk))
+  | _ => raise Unreachable);
+<INITIAL>";"{newline} =>
+  (if !pardepth = 0 then Decl (Semi yypos, SOME (Decl (Chunk yyend, NONE))) else continue());
+<INITIAL>";" => (if !pardepth = 0 then Decl (Semi yypos, NONE) else continue());
+<INITIAL>{declforms} => (if !pardepth = 0 then Decl (Chunk yypos, NONE) else continue());
+<INITIAL>{MLid} => (continue());
+<INITIAL>{newline}"End" => (EndTok (yyend-3));
+
+<string>"\\\\"|"\\\"" => (continue());
+<string>"\\"({ws}|{newline}) => (YYBEGIN stringlbrk; continue());
+<string>"\"" => (StringEnd yyend);
+<string>[^\\""\n\015]{1,10} => (continue());
+
+<stringlbrk>"\\" => (YYBEGIN string; continue());
+
+<comment,holcomment>"(*" => (inc comdepth; continue());
+<comment>"*)" => (dec comdepth; if !comdepth < 1 then Comment else continue());
+<comment>[^\n()*]{1,10} => (continue());
+
+<quote>{ProofLine} => (ProofLine (yypos, yytext));
+<quote>{HOLSTRLITstart} => (let
+  fun go () =
+    case continue() of
+      HolStrLitEnd (endpos, endq) =>
+        if strlitMatch yytext endq then
+          (YYBEGIN quote; continue())
+        else go ()
+    | EOF p => (parseError (yypos, yyend) "unterminated string"; EOF p)
+    | _ => raise Unreachable
+  in YYBEGIN holstrlit; go () end);
+
+<quote>"^"({symbol}|{ws}|"^"+) => (continue());
+<quote>"^"{newline} => (
+  yybufpos := !yybufpos - (yyend - yypos) + 1; (* unread newline *)
+  continue()
+);
+<quote>{newline}{DefinitionLabel} => (let
+  val ss = Substring.dropl Char.isSpace (Substring.full yytext)
+  val n = yypos + #2 (Substring.base ss)
+  in QDecl (DefinitionLabel (n, Substring.string ss), NONE) end);
+<quote>"(*" => (comdepth := 1; comstart := SOME (yypos, yyend); YYBEGIN holcomment; continue());
+<quote,holcomment>{quoteend} => (QuoteEnd (yypos, yytext));
+<quote,holcomment>{newline}"End" => (EndTok (yyend-3));
+<quote,holcomment>{newline}"Termination" => (TerminationTok (yyend-11));
+<quote,holcomment>{fullquoteend} => (FullQuoteEnd (yypos, yytext));
+<quote>"^" => (
+  YYBEGIN ANTIQ;
+  case continue() of
+    Antiq (aq, extra) => (YYBEGIN quote; QDecl (QuoteAntiq (yypos, aq), extra))
+  | EOF p => (parseError (p, p) "unexpected EOF"; EOF p)
+  | _ => raise Unreachable
+);
+<quote>{ws}+ => (continue());
+
+<holcomment>"*)" => (
+  dec comdepth;
+  if !comdepth < 1 then
+    case !comstart of
+      SOME (pos, _) => (comstart := NONE; YYBEGIN quote; QDecl (QuoteComment (pos, yyend), NONE))
+    | _ => raise Unreachable
+  else continue()
+);
+
+<holstrlit>"\\"{HOLSTRLITend} => (continue());
+<holstrlit>{HOLSTRLITend} => (HolStrLitEnd (yypos, yytext));
+<holstrlit>"\\\\" => (continue());
+<holstrlit>"\\"{newline} => (YYBEGIN holstrlitlbrk; continue());
+<holstrlit>"\\"{ws} => (YYBEGIN holstrlitlbrk; continue());
+<holstrlit>"\\" . => (continue());
+
+<holstrlitlbrk>"\\" => (YYBEGIN holstrlit; continue());
+
+<ANTIQ>{MLid} => (Antiq (Ident (yypos, yytext), NONE));
+<ANTIQ>"(" => (let
+  val _ = YYBEGIN INITIAL
+  val (decls, end_tok, stop, extra) =
+    parseDecls yyarg continue yyend (fn CloseParen p => SOME p | _ => NONE)
+  in Antiq (Paren {start_tok = yypos, decls = decls, end_tok = end_tok, stop = stop}, extra) end);
+<ANTIQ>({ws}|{newline})+ => (continue());
+<ANTIQ>. => (
+  parseError (yypos, yyend) "expected identifier or parenthesized group";
+  yybufpos := !yybufpos - 1; (* unread last character *)
+  Antiq (BadAntiq yypos, NONE)
+);
+
+.|{newline} => (continue());
diff --git a/tools/Holmake/HolParser.sig b/tools/Holmake/HolParser.sig
new file mode 100644
index 0000000000..ca6c5a00c9
--- /dev/null
+++ b/tools/Holmake/HolParser.sig
@@ -0,0 +1,96 @@
+signature HolParser =
+sig
+
+structure Simple: sig
+
+  datatype decl = datatype HolLex.UserDeclarations.decl
+  datatype decls = datatype HolLex.UserDeclarations.decls
+  datatype antiq = datatype HolLex.UserDeclarations.antiq
+  datatype qdecl = datatype HolLex.UserDeclarations.qdecl
+  datatype qbody = datatype HolLex.UserDeclarations.qbody
+
+  datatype topdecl
+    = TopDecl of decl
+    | EOF of int
+
+  datatype type_kind =
+      OverloadKind of {by_nametype: bool, inferior: bool}
+    | TypeKind of {pp: bool}
+
+  val destAttrs: substring -> (substring * substring list) list
+  val destMLThmBinding: substring ->
+    {keyword: substring, name: substring, attrs: substring, name_attrs: substring}
+  val destNameAttrs: substring -> substring * substring
+  val fromSS: int * substring -> int * int
+  val killEnvelopingSpace: substring -> substring
+  val kindToName: bool -> type_kind -> string
+  val parseBeginType: int * string -> (int * int -> string -> unit) ->
+    {local_: bool, kind: type_kind, keyword: substring, tyname: substring}
+  val parseDefinitionPfx: string ->
+    {keyword: substring, name: substring, attrs: substring, name_attrs: substring}
+  val parseDefnLabel: string ->
+    {name: substring option, attrs: substring, name_attrs: substring, tilde: bool}
+  val parseInductivePfx: string -> {isCo: bool, keyword: substring, thmname: substring}
+  val parseQuoteEqnPfx: string -> {bind: substring, keyword: substring, name: substring}
+  val parseQuotePfx: string -> {keyword: substring, name: substring}
+  val parseTheoremPfx: string ->
+    {isTriv: bool, keyword: substring, thmname: substring, attrs: substring, name_attrs: substring}
+
+  val mkParser:
+    {parseError: int * int -> string -> unit, pos: int, read: int -> string} ->
+    unit -> topdecl
+
+end
+
+structure ToSML: sig
+
+  type double_reader =
+    {read: int -> string, readAt: int -> int -> (int * substring -> unit) -> unit}
+  val mkDoubleReader: (int -> string) -> int -> double_reader
+
+  val mkPullTranslator:
+    {read: int -> string, filename: string, parseError: int * int -> string -> unit} ->
+    unit -> string
+
+  type strcode = {
+    aux: string -> unit,
+    regular: int * substring -> unit,
+    strcode: int * substring -> unit,
+    strstr: int * substring -> unit
+  }
+  val strstr: (string -> unit) -> int * substring -> unit
+  val strcode: (string -> unit) -> int * substring -> unit
+  val mkStrcode: (string -> unit) -> strcode
+
+  val mkPushTranslatorCore:
+    {read: int -> string, filename: string, parseError: int * int -> string -> unit} ->
+    strcode -> {
+      doDecl: bool -> int -> Simple.decl -> int,
+      feed: unit -> Simple.topdecl,
+      finishThmVal: unit -> unit,
+      regular: int * int -> unit
+    }
+
+  val mkPushTranslator:
+    {read: int -> string, filename: string, parseError: int * int -> string -> unit} ->
+    strcode -> unit -> bool
+
+end
+
+type reader = {read : unit -> char option, eof : unit -> bool}
+
+val inputFile : string -> string
+val fromString : bool -> string -> string
+
+val fileToReader : string -> reader
+val stringToReader : bool -> string -> reader
+val inputToReader : bool -> string -> (int -> string) -> reader
+val streamToReader : bool -> string -> TextIO.instream -> reader
+(* bool is true if the stream corresponds to an interactive session
+   (stdin) or a Script file. In both such situations, the magic >- and
+   Theorem-syntax transformations should be performed *)
+
+(* In inputFile and fileToReader, the determination is made on whether or
+   not the filename ends in "Script.sml" *)
+
+end
diff --git a/tools/Holmake/HolParser.sml b/tools/Holmake/HolParser.sml
new file mode 100644
index 0000000000..75bb77a724
--- /dev/null
+++ b/tools/Holmake/HolParser.sml
@@ -0,0 +1,633 @@
+structure HolParser :> HolParser =
+struct
+
+infix |>
+fun x |> f = f x
+fun mlquote s = String.concat ["\"", String.toString s, "\""]
+fun K a _ = a
+fun I a = a
+
+structure Simple = struct
+
+local
+  structure H = HolLex.UserDeclarations
+in
+  datatype decl = datatype H.decl
+  datatype decls = datatype H.decls
+  datatype antiq = datatype H.antiq
+  datatype qdecl = datatype H.qdecl
+  datatype qbody = datatype H.qbody
+
+  datatype topdecl
+    = TopDecl of decl
+    | EOF of int
+
+  fun mkParser {read, parseError, pos} = let
+    val lex = HolLex.makeLexer (read, pos) (H.STATE {
+      comdepth = ref 0, comstart = ref NONE, pardepth = ref 0, parseError = parseError})
+    val lookahead = ref NONE
+    fun go () =
+      case (case !lookahead of SOME tk => tk | NONE => lex ()) of
+        H.Decl (td, look) => (lookahead := look; TopDecl td)
+      | H.CloseParen p => (parseError (p, p + 1) ("unexpected ')'"); go ())
+      | H.EndTok _ => go ()
+      | H.QED _ => go ()
+      | H.EOF p => EOF p
+      | _ => raise H.Unreachable
+    in go end
+end
+
+fun killEnvelopingSpace s =
+  s |> Substring.dropl Char.isSpace
+    |> Substring.dropr Char.isSpace
+
+fun destNameAttrs ss =
+  if Substring.sub(ss, 0) = #"\"" then let
+    val ss' = Substring.slice(ss, 1, NONE)
+    val (nm, rest) = Substring.position "\"" ss'
+    in (nm, Substring.slice(rest, 1, NONE)) end
+  else
+    Substring.position "[" ss
+
+fun stringOfKey k =
+    case k of
+        "exclude_simps" => "simpLib.remove_simps"
+      | "exclude_frags" => "simpLib.remove_ssfrags"
+      | _ => k
+
+fun destAttrs attrs =
+  if Substring.isEmpty attrs then []
+  else
+    Substring.slice(attrs, 1, SOME (Substring.size attrs - 2))
+      |> Substring.fields (fn c => c = #",")
+      |> map (fn attr =>
+        case Substring.fields (fn c => c = #"=") (killEnvelopingSpace attr) of
+          [] => raise Fail "String.fields can't return an empty list"
+        | [key] => (killEnvelopingSpace key, [])
+        | key::vals::_ => (killEnvelopingSpace key, Substring.tokens Char.isSpace vals))
+
+fun destMLThmBinding s =
+  let
+    (* s matches {keyword}{ws}+{ident}[attrs]
+        ident is either a standard ML identifier, or something in double quotes
+        NB: If it's in double quotes, the thing in quotes might include square
+        brackets!
+
+        returns the ident, the original string corresponding to the string +
+        attributes, and the attributes as a separate list of strings
+    *)
+    val (kwordss, restss) =
+        s |> Substring.splitl Char.isAlpha
+    val ss = restss |> Substring.dropl Char.isSpace
+    val (nms, attrs) = destNameAttrs ss
+  in
+    {keyword = kwordss, name_attrs = ss, name = nms, attrs = attrs}
+  end
+
+fun fromSS (base, ss) = let
+  val (_, lo, len) = Substring.base ss
+  in (base + lo, base + lo + len) end
+
+datatype type_kind
+  = OverloadKind of {inferior: bool, by_nametype: bool}
+  | TypeKind of {pp: bool}
+
+fun kindToName local_ kind =
+  (if local_ then "temp_" else "") ^
+  (case kind of
+    OverloadKind {inferior, by_nametype} =>
+    (if inferior then "inferior_" else "") ^
+    "overload_on" ^
+    (if by_nametype then "_by_nametype" else "")
+  | TypeKind {pp} => "type_abbrev" ^ (if pp then "_pp" else ""))
+
+(* ("Type"|"Overload"){ws}+({alphaMLid}|{quotedsymbolid})("["{alphaMLid_list}"]")?{ws}*"=" *)
+fun parseBeginType (start, text) parseError = let
+  val s = Substring.substring(text, 0, size text - 1) (* drop = *)
+    |> Substring.dropr Char.isSpace (* drop wspace after name *)
+  val {keyword, name, attrs, ...} = destMLThmBinding s
+  val isOverload = Substring.size keyword = 8
+  fun expectNoArgs [] = ()
+    | expectNoArgs (v :: _) = parseError (fromSS (start, v)) "expected no arguments"
+  val inferior = ref false
+  val local_ = ref false
+  val pp = ref false
+  val by_nametype = ref false
+  fun parseAttr (k, vs) =
+    case (Substring.string k, isOverload) of
+      ("inferior", true) => (expectNoArgs vs; inferior := true)
+    | ("local", _) => (expectNoArgs vs; local_ := true)
+    | ("pp", false) => (expectNoArgs vs; pp := true)
+    | ("by_nametype", true) => (expectNoArgs vs; by_nametype := true)
+    | (sk, _) => parseError (fromSS (start, k)) ("unexpected attribute '"^sk^"'")
+  val _ = app parseAttr (destAttrs attrs)
+  val kind =
+    if isOverload then OverloadKind {inferior = !inferior, by_nametype = !by_nametype}
+    else TypeKind {pp = !pp}
+  in {local_ = !local_, kind = kind, keyword = keyword, tyname = name} end
+
+(* {Theorempfx}{ws}*":"  or  {Theorempfx}({ws}|{newline})+"="
+where Theorempfx = ("Theorem"|"Triviality"){ws}+{alphaMLid}({ws}*"["{alphaMLid_list}"]")?; *)
+fun parseTheoremPfx text = let
+  val s = Substring.substring(text, 0, size text - 1) (* drop : or = *)
+    |> Substring.dropr Char.isSpace (* drop wspace between name and ] *)
+  val {keyword, name, attrs, name_attrs} = destMLThmBinding s
+  val isTriv = Substring.size keyword = 10
+  in {isTriv = isTriv, keyword = keyword,
+      thmname = name, attrs = attrs, name_attrs = name_attrs} end
+
+(* Inductivepfx = ("Co")?"Inductive"{ws}+{alphaMLid}{ws}*":"; *)
+fun parseInductivePfx text = let
+  val (keyword, s) = Substring.substring(text, 0, size text - 1) (* drop : *)
+    |> Substring.splitl (not o Char.isSpace) (* split keyword *)
+  val name = s
+    |> Substring.dropl Char.isSpace (* space before name *)
+    |> Substring.dropr Char.isSpace (* space after name *)
+  in {isCo = Substring.size keyword = 11, keyword = keyword, thmname = name} end
+
+(* Definitionpfx =
+"Definition"{ws}+{alphaMLid}({ws}*"["{optallws}{defn_attribute_list}"]")?{ws}*":"; *)
+fun parseDefinitionPfx text = let
+  val s = Substring.substring(text, 0, size text - 1) (* drop : *)
+    |> Substring.dropr Char.isSpace (* drop wspace after name *)
+  in destMLThmBinding s end
+
+(* Quote_pfx = "Quote"{ws}+{QUALalphaMLid}{ws}*":"; *)
+fun parseQuotePfx text = let
+  val name = Substring.substring(text, 6, size text - 7) (* drop :, "Quote" + next ws char *)
+    |> Substring.dropl Char.isSpace (* space before name *)
+    |> Substring.dropr Char.isSpace (* space after name *)
+  in {keyword = Substring.substring(text, 0, 5), name = name} end
+
+(* Quote_eqnpfx = "Quote"{ws}+{alphaMLid}{ws}*"="{ws}*{QUALalphaMLid}{ws}*":"; *)
+fun parseQuoteEqnPfx text = let
+  val (left, right) = Substring.substring(text, 6, size text - 7) (* drop :, Quote, next ws char *)
+    |> Substring.dropl Char.isSpace (* space before name *)
+    |> Substring.dropr Char.isSpace (* space after name *)
+    |> Substring.position "="
+  val bind = left |> Substring.dropr Char.isSpace
+  val name = Substring.slice(right, 1, NONE) |> Substring.dropl Char.isSpace
+  in {keyword = Substring.substring(text, 0, 5), bind = bind, name = name} end
+
+(* DefinitionLabel = "["{ws}*{DefinitionLabelID}?("["{alphaMLid_list}"]")?{ws}*":"?{ws}*"]"; *)
+fun parseDefnLabel text = let
+  val ss = Substring.full text
+    |> Substring.dropr Char.isSpace
+    |> (fn s => Substring.slice (s, 1, SOME (Substring.size s - 2)))
+    |> Substring.dropl Char.isSpace
+    |> Substring.dropr (fn c => Char.isSpace c orelse c = #":")
+  val (ss, tilde) =
+    case Substring.getc ss of
+      SOME (#"~", ss) => (ss, true)
+    | _ => (ss, false)
+  val (name, attrs) = destNameAttrs ss
+  val str = Substring.string name
+  val name =
+    if str = "/\092" orelse str = "\226\136\167" orelse str = "" then NONE
+    else SOME name
+  in {tilde = tilde, name = name, attrs = attrs, name_attrs = ss} end
+
+end
+
+structure ToSML = struct
+
+  type double_reader = {
+    read: int -> string,
+    readAt: int -> int -> (int * substring -> unit) -> unit
+  }
+
+  (*
+    This function takes an input stream `read: int -> string` and returns another stream with the
+    same type, along with a function `readAt (from: int) (to: int) (push: int * substring -> unit)`
+    which is another stream, yielding values that have already been yielded from the first stream.
+    Internally it maintains a buffer of results that `read` has yielded, indexed by byte positions
+    (starting at `pos`).
+
+    `readAt from to push` is a request to skip forward to position `from`, then yield the bytes
+    `from .. to` to the callback `push`. This function can only be called once for these positions;
+    the next call to `readAt` must have a `from` larger than the previous `to` value and `to` must
+    be no larger than the total of all bytes provided by the main stream `read`.
+
+    `push (bufstart, chunk)` is called repeatedly to output each chunk of the response, where
+    `bufstart + chunk.start` is the position of the start of `chunk` in the stream.
+  *)
+  fun mkDoubleReader read pos: double_reader = let
+    val inbox = ref (pos, [])
+    val outbox = ref (pos, [])
+    val pos = ref pos
+    fun read' n = let
+      val buf = read n
+      val _ = if buf = "" then () else let
+        val (ahead, backlog) = !inbox
+        in inbox := (ahead + size buf, buf :: backlog) end
+      in buf end
+    fun readAt from to push = let
+      fun checkInbox from = if from = to then () else let
+        fun moveToOutbox [] mid acc = raise Fail "unreachable"
+          | moveToOutbox (chunk :: rest) mid acc = let
+            val mid' = mid - size chunk
+            in
+              if mid' <= from then printOutbox mid' chunk mid acc from
+              else moveToOutbox rest mid' (chunk :: acc)
+            end
+        val (lead, bufs) = !inbox
+        val _ = if to <= lead then () else raise Fail "main reader has not yielded this much yet"
+        in inbox := (lead, []); moveToOutbox bufs lead [] end
+      and printOutbox trail chunk trail' rest from =
+        if to <= trail' then (
+          push (trail, Substring.substring (chunk, from - trail, to - from));
+          outbox := (trail, chunk :: rest)
+        ) else (
+          push (trail, Substring.substring (chunk, from - trail, trail' - from));
+          case rest of
+            [] => checkInbox trail'
+          | chunk' :: rest' => printOutbox trail' chunk' (trail' + size chunk') rest' trail'
+        )
+      fun dropOutbox [] _ = checkInbox from
+        | dropOutbox (chunk :: rest) trail = let
+          val trail' = trail + size chunk
+          in
+            if trail' <= from then dropOutbox rest trail'
+            else printOutbox trail chunk trail' rest from
+          end
+      val _ = if from <= to then () else raise Fail "readAt: to < from"
+      val (back, bufs) = !outbox
+      val _ = if back <= from then () else raise Fail "segment has already been yielded"
+      in dropOutbox bufs back end
+    in {read = read', readAt = readAt} end
+
+  type strcode = {
+    aux: string -> unit,
+    regular: int * substring -> unit,
+    strcode: int * substring -> unit,
+    strstr: int * substring -> unit
+  }
+
+  local
+    fun encoder f push (_, s) = let
+      val (s, start, len) = Substring.base s
+      val stop = start + len
+      fun loop start p =
+        if p = stop then
+          if start = p then () else push (String.substring (s, start, p - start))
+        else
+          case f (String.sub (s, p)) of
+            NONE => loop start (p+1)
+          | SOME r => (
+            if start = p then () else push (String.substring (s, start, p - start));
+            push r;
+            loop (p+1) (p+1))
+      in loop start start end
+  in
+    val strstr = encoder (fn ch =>
+      if ch < #"\128" then NONE else SOME (AttributeSyntax.bslash_escape ch))
+    val strcode = encoder (fn
+        #"\\" => SOME "\\\\"
+      | #"\"" => SOME "\\\""
+      | #"\n" => SOME "\\n\\\n\\"
+      | ch => if Char.isPrint ch then NONE else SOME (AttributeSyntax.bslash_escape ch))
+  end
+
+  fun mkStrcode push: strcode = {
+    regular = fn s => push (Substring.string (#2 s)),
+    aux = push,
+    strstr = strstr push,
+    strcode = strcode push
+  }
+
+  fun mkPushTranslatorCore {read, filename, parseError}
+      ({regular, aux, strstr, strcode = strcode0}:strcode) = let
+    open Simple
+    val ss = Substring.string
+    val full = Substring.full
+    val cat = Substring.concat
+    val filename = ref filename
+    val {read, readAt} = mkDoubleReader read 0
+    val feed = mkParser {read = read, pos = ~1 (* fix for mllex bug *), parseError = parseError}
+    val lookahead = ref NONE
+    fun feed' () = case !lookahead of SOME tk => tk | NONE => feed ()
+    val inThmVal = ref false
+    fun finishThmVal () = if !inThmVal then (aux ");"; inThmVal := false) else ()
+    val line = ref (0, 0)
+    fun countlines (p, s) = let
+      val lastline = Substring.dropr (fn c => c <> #"\n") s
+      in
+        if Substring.isEmpty lastline then ()
+        else line := (
+          Substring.foldr (fn (c, n) => if c = #"\n" then n+1 else n) (#1 (!line)) lastline,
+          let val (_, start, len) = Substring.base lastline in p + start + len end)
+      end
+    fun wrap f (start, stop) = if start = stop then () else
+      readAt start stop (fn s => (countlines s; f s))
+    val regular = wrap regular
+    val strcode = wrap strcode0
+    val strstr = wrap strstr
+    val regular' = regular o fromSS
+    val strcode' = strcode o fromSS
+    val strstr' = strstr o fromSS
+    fun locpragma pos = let
+      val (line, start) = !line
+      in
+        aux (concat [
+          " (*#loc ", Int.toString (line + 1), " ", Int.toString (pos - start + 1), "*)"])
+        (* NB: the initial space is critical, or else the comment might not be recognised
+           when prepended by a paren or symbol char.  --KW
+           See cvs log comment at rev 1.2 of src/parse/base_tokens.lex *)
+      end
+    fun quote (start, stop) = (locpragma start; strcode (start, stop))
+    fun magicBind name =
+      aux (" " ^ Systeml.bindstr (concat ["val ", name, " = DB.fetch \"-\" \"", name,
+        "\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;"]) ^ ";")
+    fun doThmAttrs false p attrs name_attrs = aux (ss name_attrs)
+      | doThmAttrs true p attrs name_attrs =
+        if Substring.isEmpty attrs then
+          (aux (ss name_attrs); aux "[local]")
+        else (
+          aux (ss (Substring.slice (name_attrs, 0, SOME (Substring.size name_attrs - 1))));
+          aux ",local]")
+    fun doQuoteCore start ds stop f = case ds of
+        [] => quote (start, stop)
+      | QuoteComment _ :: rest => doQuoteCore start rest stop f
+      | QuoteAntiq (_, BadAntiq _) :: rest => doQuoteCore start rest stop f
+      | QuoteAntiq (p, Ident (idstart, id)) :: rest => (
+        quote (start, p);
+        aux "\", ANTIQUOTE "; regular (idstart, idstart + size id); aux ", QUOTE \"";
+        doQuoteCore (idstart + size id) rest stop f)
+      | QuoteAntiq (p, Paren {start_tok, decls, end_tok, stop = pstop}) :: rest => let
+        val Decls {start = dstart, decls, stop = dstop} = decls
+        in
+          quote (start, p); aux "\", ANTIQUOTE ";
+          case end_tok of
+            NONE => (doDecls start_tok decls dstop; aux ")")
+          | SOME _ => doDecls start_tok decls pstop;
+          aux ", QUOTE \"";
+          doQuoteCore pstop rest stop f
+        end
+      | DefinitionLabel (l as (p, t)) :: rest =>
+        case f of
+          NONE => doQuoteCore start rest stop f
+        | SOME g => (quote (start, p); g l; doQuoteCore (p + size t) rest stop f)
+    and doQuote (QBody {start, toks, stop}) =
+      (aux "[QUOTE \""; doQuoteCore start toks stop NONE; aux "\"]")
+    and doQuoteConj (QBody {start, toks, stop}) f = let
+      val first = ref true
+      val strcode1 = wrap (fn (p as (_, s)) => (
+        if !first then first := Substring.isEmpty (Substring.dropl Char.isSpace s) else ();
+        strcode0 p))
+      fun doQuote0 start toks =
+        case toks of
+          DefinitionLabel (l as (p, t)) :: rest => (
+          strcode1 (start, p); f (!first) l;
+          doQuoteCore (p + size t) rest stop (SOME (f false)))
+        | QuoteComment (p, stop) :: rest =>
+          (strcode1 (start, p); strcode (p, stop); doQuote0 stop rest)
+        | _ => doQuoteCore start toks stop (SOME (f false))
+      in aux "[QUOTE \"("; locpragma start; doQuote0 start toks; aux ")\"]" end
+    and doDecl eager pos d = case d of
+        DefinitionDecl {head = (p, head), quote, termination, stop, ...} => let
+        val {keyword, name, attrs, name_attrs} = parseDefinitionPfx head
+        val attrs = destAttrs attrs
+        val indThm =
+          case List.find (fn (k,v) => Substring.compare (k, full "induction") = EQUAL) attrs of
+            SOME (_, s::_) => ss s
+          | _ =>
+            if Substring.isSuffix "_def" name then
+              cat [Substring.slice (name, 0, SOME (Substring.size name - 4)), full "_ind"]
+            else if Substring.isSuffix "_DEF" name then
+              cat [Substring.slice (name, 0, SOME (Substring.size name - 4)), full "_IND"]
+            else cat [name, full "_ind"]
+        in
+          regular (pos, p); finishThmVal ();
+          aux "val "; regular' (p, name); aux " = ";
+          if !filename = "" then aux "TotalDefn.qDefine"
+          else app aux [
+            "TotalDefn.located_qDefine (DB_dtype.mkloc (",
+              mlquote (!filename), ", ",
+              Int.toString (#1 (!line) + 1) ^ ", true))"];
+          app aux [" \"", ss name_attrs, "\" "]; doQuote quote;
+          case termination of
+            NONE => aux " NONE;"
+          | SOME {decls = Decls {start = dstart, decls = decls, stop = dstop}, ...} =>
+            (aux " (SOME ("; doDecls dstart decls dstop; aux "));");
+          magicBind indThm;
+          stop
+        end
+      | DatatypeDecl {head = (p, head), quote, stop, ...} => (
+          regular (pos, p); finishThmVal ();
+          aux "val _ = bossLib.Datatype "; doQuote quote; aux ";";
+          stop)
+      | QuoteDecl {head = (p, head), quote, stop, ...} => let
+        val {keyword, name} = parseQuotePfx head
+        in
+          regular (pos, p); finishThmVal ();
+          aux "val _ = "; regular' (p, name); aux " "; doQuote quote; aux ";";
+          stop
+        end
+      | QuoteEqnDecl {head = (p, head), quote, stop, ...} => let
+        val {keyword, name, bind} = parseQuoteEqnPfx head
+        in
+          regular (pos, p); finishThmVal ();
+          aux "val "; regular' (p, bind); aux " = ";
+          regular' (p, name); aux " "; doQuote quote; aux ";";
+          stop
+        end
+      | InductiveDecl {head = (p, head), quote, stop, ...} => let
+        val {isCo, keyword, thmname = stem} = parseInductivePfx head
+        val (entryPoint, indSuffix) =
+          if isCo then ("CoIndDefLib.xHol_coreln", "_coind") else ("IndDefLib.xHol_reln", "_ind")
+        val conjIdx = ref 1
+        val conjs = ref []
+        fun collect first (p, lab) = (
+          if first then () else (aux ") /\\\\ ("; conjIdx := !conjIdx + 1);
+          case parseDefnLabel lab of
+            {tilde, name = SOME name, name_attrs, ...} =>
+            conjs := (!conjIdx, tilde, name, name_attrs) :: !conjs
+          | _ => ()
+        )
+        in
+          regular (pos, p); finishThmVal ();
+          app aux ["val (", ss stem, "_rules,", ss stem, indSuffix, ",",
+            ss stem, "_cases) = ", entryPoint, " \"", ss stem, "\" "];
+          doQuoteConj quote collect; aux ";";
+          magicBind (cat [stem, full "_strongind"]);
+          app (fn (i, tilde, name, name_attrs) => let
+            val f = if tilde then fn s => app aux [ss stem, "_", s] else aux
+            in
+              aux " val "; f (ss name); aux " = boolLib.save_thm(\""; f (ss name_attrs);
+              app aux ["\", Drule.cj ", Int.toString i, " ",
+                ss stem, "_rules handle HOL_ERR _ => boolTheory.TRUTH);"]
+            end) (rev (!conjs));
+          stop
+        end
+      | BeginType (p, head) => let
+        val {local_, kind, keyword, tyname} = parseBeginType (p, head) parseError
+        val fnm = kindToName local_ kind
+        in
+          regular (pos, p); finishThmVal ();
+          app aux ["val _ = Parse.", fnm, "(\""]; strstr' (p, tyname); aux "\",";
+          inThmVal := true; p + size head
+        end
+      | BeginSimpleThm (p, head) => let
+        val {isTriv, keyword, thmname, attrs, name_attrs} = parseTheoremPfx head
+        in
+          regular (pos, p); finishThmVal ();
+          aux "val "; regular' (p, thmname); aux " = boolLib.save_thm(\"";
+          doThmAttrs isTriv p attrs name_attrs; aux "\","; inThmVal := true;
+          p + size head
+        end
+      | TheoremDecl {head = (p, head), quote, proof_tok, body, stop, ...} => let
+        val {isTriv, keyword, thmname, attrs, name_attrs} = parseTheoremPfx head
+        val goalabs = "(fn HOL__GOAL__foo => (";
+        val Decls {start = dstart, decls, stop = dstop} = body
+        in
+          regular (pos, p); finishThmVal ();
+          aux "val "; regular' (p, thmname); aux " = Q.store_thm(\"";
+          doThmAttrs isTriv p attrs name_attrs; aux "\", ";
+          doQuote quote; aux ", ";
+          case proof_tok of
+            SOME (p, tok) => let
+            fun ofKey "exclude_simps" = "simpLib.remove_simps"
+              | ofKey "exclude_frags" = "simpLib.remove_ssfrags"
+              | ofKey k = k
+            fun mktm1 (k,vals) = ofKey (ss k) ^ " [" ^
+              String.concatWith "," (map (mlquote o ss) vals) ^ "]"
+            fun mktm kv [] = mktm1 kv
+              | mktm kv (kv2::xs) = mktm1 kv ^ " o " ^ mktm kv2 xs
+            val () = case destAttrs (#2 (destNameAttrs (full tok))) of
+              [] => ()
+            | kv::attrs => aux ("BasicProvers.with_simpset_updates (" ^ mktm kv attrs ^ ") ")
+            val n = #1 (!line)
+            val _ = readAt p (p + size tok) countlines
+            in aux goalabs; aux (CharVector.tabulate (#1 (!line) - n, (fn _ => #"\n"))) end
+          | _ => aux goalabs;
+          doDecls dstart decls dstop; aux ") HOL__GOAL__foo));";
+          stop
+        end
+      | Chunk p =>
+        if !inThmVal then
+          (regular (pos, p); aux ");"; inThmVal := false; p)
+        else if eager then
+          (regular (pos, p); p)
+        else
+          pos
+      | Semi p =>
+        if !inThmVal then
+          (regular (pos, p); aux ")"; inThmVal := false; regular (p, p+1); p+1)
+        else if eager then
+          (regular (pos, p+1); p+1)
+        else
+          pos
+      | FullQuote {head = (p, head), type_q, quote, stop, ...} => (
+        regular (pos, p);
+        aux (case type_q of NONE => "(Parse.Term " | SOME _ => "(Parse.Type ");
+        doQuote quote; aux ")";
+        stop)
+      | Quote {head = (p, _), quote, stop, ...} => (regular (pos, p); doQuote quote; stop)
+      | String (start, stop) => (regular (pos, start); strstr (start, stop); stop)
+      | LinePragma p => (regular (pos, p); aux (Int.toString (#1 (!line) + 1)); p + 7)
+      | LinePragmaWith (p, text) => let
+        val num = Substring.substring(text, 7, size text - 8)
+        in
+          regular (pos, p);
+          case Int.fromString (Substring.string num) of
+            NONE => parseError (fromSS (p, num)) "expected an integer"
+          | SOME num => line := (fn (_, pos) => (num - 1, pos)) (!line);
+          aux " "; p + size text
+        end
+      | FilePragma p => (regular (pos, p); aux (mlquote (!filename)); p + 7)
+      | FilePragmaWith (p, text) => (
+          regular (pos, p);
+          filename := String.substring(text, 7, size text - 8);
+          aux " "; p + size text)
+    and doDecls start [] stop = regular (start, stop)
+      | doDecls start (d :: ds) stop = doDecls (doDecl false start d) ds stop
+    in {
+      feed = feed',
+      regular = regular,
+      finishThmVal = finishThmVal,
+      doDecl = doDecl
+    } end
+
+  fun mkPushTranslator args strcode = let
+    open Simple
+    val {feed, regular, finishThmVal, doDecl, ...} = mkPushTranslatorCore args strcode
+    val pos = ref 0
+    in fn () =>
+      case feed () of
+        TopDecl d => (pos := doDecl true (!pos) d; false)
+      | Simple.EOF p => (regular (!pos, p); finishThmVal (); pos := p; true)
+    end
+
+  fun mkPullTranslator args = let
+    val queue = ref []
+    val atEnd = ref false
+    val push = mkPushTranslator args (mkStrcode (fn s => queue := s :: !queue))
+    fun loop () =
+      case !queue of
+        s :: rest => (queue := rest; s)
+      | [] => if !atEnd then "" else (
+        atEnd := push ();
+        queue := rev (!queue);
+        loop ())
+    in loop end
+
+end
+
+open HOLFileSys
+type reader = {read : unit -> char option, eof : unit -> bool}
+
+fun exhaust_parser (read, close) =
+  let
+    fun recurse acc =
+      case read () of
+          "" => (close(); String.concat (List.rev acc))
+        | s => recurse (s::acc)
+  in
+    recurse []
+  end
+
+fun mkstate b = {inscriptp = b, quotefixp = false}
+
+fun file_to_parser fname = let
+  val instrm = openIn fname
+  (* val isscript = String.isSuffix "Script.sml" fname *)
+  val read = ToSML.mkPullTranslator
+    {read = fn n => input instrm, filename = fname, parseError = K (K ())}
+  in (read, fn () => closeIn instrm) end
+
+fun string_to_parser isscriptp s = let
+  val sr = ref s
+  fun str_read _ = (!sr before sr := "")
+  val read = ToSML.mkPullTranslator {read = str_read, filename = "", parseError = K (K ())}
+  in (read, I) end
+
+fun input_to_parser isscriptp fname inp = let
+  val read = ToSML.mkPullTranslator {read = inp, filename = fname, parseError = K (K ())}
+  in (read, I) end
+
+fun stream_to_parser isscriptp fname strm =
+  input_to_parser isscriptp fname (fn n => input strm)
+
+fun inputFile fname = exhaust_parser (file_to_parser fname)
+fun fromString b s = exhaust_parser (string_to_parser b s)
+
+fun mkReaderEOF (read, close) = let
+  val i = ref 0
+  val s = ref ""
+  val sz = ref 0
+  val eofp = ref false
+  fun pull () = (s := read(); sz := size (!s); i := 0;
+                 if !sz = 0 then (eofp := true; close()) else ())
+  fun doit () =
+    if !eofp then NONE
+    else if !i < !sz then SOME (String.sub(!s,!i)) before i := !i + 1
+    else (pull(); doit())
+  fun eof () = !eofp
+  in {read = doit, eof = eof} end
+
+fun fileToReader fname = mkReaderEOF (file_to_parser fname)
+fun stringToReader b s = mkReaderEOF (string_to_parser b s)
+fun inputToReader b fnm inp = mkReaderEOF (input_to_parser b fnm inp)
+fun streamToReader b fnm strm = mkReaderEOF (stream_to_parser b fnm strm)
+
+end
diff --git a/tools/Holmake/Holdep.sml b/tools/Holmake/Holdep.sml
index 41251375e6..6d8c8a86ec 100644
--- a/tools/Holmake/Holdep.sml
+++ b/tools/Holmake/Holdep.sml
@@ -124,7 +124,7 @@ fun encode_for_HOLMKfile {tgt, deps} =
 
 fun uqfname_holdep fname =
   let
-    val reader = QFRead.fileToReader fname
+    val reader = HolParser.fileToReader fname
   in
     Holdep_tokens.reader_deps (fname, #read reader)
   end
diff --git a/tools/Holmake/QFRead.sig b/tools/Holmake/QFRead.sig
index 08487c44e4..614a12f309 100644
--- a/tools/Holmake/QFRead.sig
+++ b/tools/Holmake/QFRead.sig
@@ -17,7 +17,7 @@ val streamToReader : bool -> string -> TextIO.instream -> reader
 
    The strings in {input,stream}ToReader allow the specification of the
    filename associated with the stream; the quotation filter will quote
-   this name back to the user with the #(FNAME) directive.
+   this name back to the user with the #(FILE) directive.
 *)
 
 (* In inputFile and fileToReader, the determination is made on whether or
diff --git a/tools/Holmake/QuoteFilter b/tools/Holmake/QuoteFilter
index 41abb0a363..42f6a28c37 100644
--- a/tools/Holmake/QuoteFilter
+++ b/tools/Holmake/QuoteFilter
@@ -266,13 +266,13 @@ ProofLine =
        | SOME i => setlinenum i yyarg;
      (yypos, " "))
 );
-<INITIAL> "#(FNAME)" => (
+<INITIAL> "#(FILE)" => (
   if quotefix then (yypos,yytext)
   else (yypos, "\"" ^ !scriptfilename ^ "\"")
 );
-<INITIAL> "#(FNAME="[-A-Za-z0-9/$()_.]+")" => (
+<INITIAL> "#(FILE="[-A-Za-z0-9/$()_.]+")" => (
   if quotefix then (yypos,yytext)
-  else (scriptfilename := String.substring(yytext,8,size yytext-9);
+  else (scriptfilename := String.substring(yytext,7,size yytext-8);
         (yypos, " "))
 );
 <INITIAL,thmval,TERMINATION_VAL>"(*" => (
@@ -322,7 +322,7 @@ ProofLine =
   (yypos,
    if inscript andalso not quotefix then
      let
-       infix |> 
+       infix |>
        fun extract (s,p) l =
            if List.exists (fn (a,_) => a = s) l then
              (p, List.filter (fn (a,_) => a <> s) l)
@@ -354,7 +354,7 @@ ProofLine =
 (
   if inscript andalso not quotefix then
     let
-      infix |> 
+      infix |>
       val pfx = mlswitch (!mltype_stack) "" "" ");"
       val s0 = String.extract(yytext,0,SOME (size yytext - 1)) (* drop colon *)
       val s = s0 |> Substring.full |> Substring.dropr Char.isSpace
@@ -828,7 +828,7 @@ ProofLine =
 
 <quote,tmquote,tyquote,defnquote,datatypequote,rawquote>"^"{symbol} => ((yypos, (ECHO yyarg yytext)));
 <defnquote0>"^"{symbol} => (
-  (yypos, if quotefix then yytext 
+  (yypos, if quotefix then yytext
           else (inc conjcount; YYBEGIN defnquote; yytext))
 );
 <quote,tmquote,tyquote,defnquote0,defnquote,datatypequote,rawquote>{newline} =>
@@ -857,7 +857,7 @@ ProofLine =
      YYBEGIN INITIAL;
      nextline yyarg (yypos + size yytext);
      if quotefix then yytext
-     else 
+     else
        (if !inddefp then ")" else "") ^ "\"\n] NONE; " ^ magic_bind yyarg ^
        String.concat (List.map (extra_binds (!stem)) (!labelidxs))
     )
diff --git a/tools/Holmake/hmcore.ML b/tools/Holmake/hmcore.ML
index 3e1c83ce86..74f33c55dd 100644
--- a/tools/Holmake/hmcore.ML
+++ b/tools/Holmake/hmcore.ML
@@ -21,10 +21,10 @@ in
   myuse (OS.Path.concat(hmakedir, "poly")) "HFS_NameMunge.sml";
   app appthis ["HOLFileSys", "regexpMatch", "parse_glob",
                "Holdep_tokens", "AttributeSyntax"] ;
-  app (myuse hmakedir) ["QuoteFilter.sml", "Holmake_tools_dtype.sml",
+  app (myuse hmakedir) ["HolLex.sml", "Holmake_tools_dtype.sml",
                         "terminal_primitives.sig",
                         "poly-terminal-prims.ML"];
-  app appthis ["QFRead", "Holdep", "Holmake_tools", "internal_functions",
+  app appthis ["HolParser", "Holdep", "Holmake_tools", "internal_functions",
                "Holmake_types",
                "ReadHMF"]
 end;
diff --git a/tools/Holmake/hmcore.mlb b/tools/Holmake/hmcore.mlb
index fc0b5c8a1e..3103264113 100644
--- a/tools/Holmake/hmcore.mlb
+++ b/tools/Holmake/hmcore.mlb
@@ -15,9 +15,9 @@ Holdep_tokens.sig
 Holdep_tokens.sml
 AttributeSyntax.sig
 AttributeSyntax.sml
-QuoteFilter.sml
-QFRead.sig
-QFRead.sml
+HolLex.sml
+HolParser.sig
+HolParser.sml
 Holdep.sig
 Holdep.sml
 regexpMatch.sig
diff --git a/tools/Holmake/holdeptool.sml b/tools/Holmake/holdeptool.sml
index 9939e2505a..0ddbf6c6b8 100644
--- a/tools/Holmake/holdeptool.sml
+++ b/tools/Holmake/holdeptool.sml
@@ -23,7 +23,7 @@ fun main() = let
                  handle LEX_ERROR s => diewith("Lexical error: " ^ s)
                       | e => diewith ("Exception: "^General.exnMessage e))
         | ["-h"] => usage ok
-        | [fname] => (reader_deps (fname, #read (QFRead.fileToReader fname))
+        | [fname] => (reader_deps (fname, #read (HolParser.fileToReader fname))
                       handle LEX_ERROR s => diewith("Lexical error: " ^ s)
                            | e => diewith ("Exception: "^General.exnMessage e))
         | _ => usage die
diff --git a/tools/Holmake/poly-holdeptool.ML b/tools/Holmake/poly-holdeptool.ML
index a3f1cf3472..17c870e044 100644
--- a/tools/Holmake/poly-holdeptool.ML
+++ b/tools/Holmake/poly-holdeptool.ML
@@ -16,9 +16,9 @@ use "Systeml.sig";
 use "../../tools-poly/Holmake/Systeml.sml";
 use "AttributeSyntax.sig";
 use "AttributeSyntax.sml";
-use "QuoteFilter.sml";
-use "QFRead.sig";
-use "QFRead.sml";
+use "HolLex.sml";
+use "HolParser.sig";
+use "HolParser.sml";
 use "holdeptool.sml";
 
 val main = holdeptool.main
diff --git a/tools/Holmake/tests/quote-filter/expected-mosml b/tools/Holmake/tests/quote-filter/expected-mosml
index a6e135ec56..edbf724b80 100644
--- a/tools/Holmake/tests/quote-filter/expected-mosml
+++ b/tools/Holmake/tests/quote-filter/expected-mosml
@@ -3,12 +3,12 @@
 (Parse.Term [QUOTE " (*#loc 3 3*)\"foo\""])
 [QUOTE " (*#loc 4 2*)foo = #\"^`\""]
 [QUOTE " (*#loc 5 2*)\"\\\"\""]
-(Parse.Term [QUOTE " (*#loc 6 3*)\t"])
+(Parse.Term [QUOTE " (*#loc 6 3*)\009"])
 (Parse.Term [QUOTE " (*#loc 7 3*)(* foo"])
-[QUOTE " (*#loc 8 2*)^"]
+[QUOTE " (*#loc 8 2*)^^"]
 "\"" (Parse.Term [QUOTE " (*#loc 9 8*)foo"])
 "\\" [QUOTE " (*#loc 10 7*)foo"]
-[QUOTE " (*#loc 11 2*)putting unescaped backticks into ", ANTIQUOTE ((antiquotes #"`")),QUOTE " (*#loc 11 53*) is fine"]
+[QUOTE " (*#loc 11 2*)putting unescaped backticks into ", ANTIQUOTE (antiquotes #"`"), QUOTE " (*#loc 11 53*) is fine"]
 (Parse.Term [QUOTE " (*#loc 12 3*)foo\n\
 \bar"])
 (Parse.Term [QUOTE " (*#loc 14 3*)\"an embedded string with \\\n\
@@ -21,74 +21,75 @@
 [QUOTE " (*#loc 21 2*)s1 ^^\n\
 \s2"]
 (* ` *)
-[QUOTE " (*#loc 24 2*)", ANTIQUOTE ((fromMLnum nm)),QUOTE " (*#loc 24 17*) (* *) "];
+[QUOTE " (*#loc 24 2*)", ANTIQUOTE (fromMLnum nm), QUOTE " (*#loc 24 17*) (* *) "];
 (* (*  *) `;*)
 
-val (even_rules,even_ind,even_cases) = (fn q => fn _ => IndDefLib.xHol_reln "even" q) [QUOTE "( (*#loc 27 16*)\n\
-\ even 0) /\\ (\n\
-\ (!n. even n ==> odd (n + 1))) /\\ (\n\
-\\n\
-\  (!m. odd m ==> even (m + 1)))"
-] NONE; val even_strongind = DB.fetch "-" "even_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;val even_0 = boolLib.save_thm("even_0[simp]", Drule.cj 1 even_rules handle HOL_ERR _ => boolTheory.TRUTH);val even_suc = boolLib.save_thm("even_suc", Drule.cj 3 even_rules handle HOL_ERR _ => boolTheory.TRUTH);
+val (even_rules,even_ind,even_cases) = IndDefLib.xHol_reln "even" [QUOTE "( (*#loc 27 16*)\n\
+\ (*#loc 28 12*) even 0\n\
+\) /\\ ( (*#loc 29 5*) (!n. even n ==> odd (n + 1))\n\
+\) /\\ ( (*#loc 30 12*)\n\
+\  (!m. odd m ==> even (m + 1))\n\
+\)"]; val even_strongind = DB.fetch "-" "even_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;; val even_0 = boolLib.save_thm("even_0[simp]", Drule.cj 1 even_rules handle HOL_ERR _ => boolTheory.TRUTH); val even_suc = boolLib.save_thm("even_suc", Drule.cj 3 even_rules handle HOL_ERR _ => boolTheory.TRUTH);
 
 val foo = TotalDefn.qDefine "foo" [QUOTE " (*#loc 34 16*)\n\
-\  foo x = if x < 2 then 1 else x * foo (x - 1)"
-] NONE; val foo_ind = DB.fetch "-" "foo_ind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;
+\  foo x = if x < 2 then 1 else x * foo (x - 1)\n\
+\"] NONE; val foo_ind = DB.fetch "-" "foo_ind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;
 
-val (compile_rel_rules,compile_rel_ind,compile_rel_cases) = (fn q => fn _ => IndDefLib.xHol_reln "compile_rel" q) [QUOTE "( (*#loc 38 23*)\n\
+val (compile_rel_rules,compile_rel_ind,compile_rel_cases) = IndDefLib.xHol_reln "compile_rel" [QUOTE "( (*#loc 38 23*)\n\
 \  (* (*  *) *)\n\
-\\n\
-\  compile_rel foo bar) /\\ (\n\
-\\n\
-\  compile_rel foo bar)"
-] NONE; val compile_rel_strongind = DB.fetch "-" "compile_rel_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;val compile_rel_Var = boolLib.save_thm("compile_rel_Var", Drule.cj 1 compile_rel_rules handle HOL_ERR _ => boolTheory.TRUTH);val compile_rel_Ret = boolLib.save_thm("compile_rel_Ret", Drule.cj 2 compile_rel_rules handle HOL_ERR _ => boolTheory.TRUTH);
+\ (*#loc 40 8*)\n\
+\  compile_rel foo bar\n\
+\) /\\ ( (*#loc 42 8*)\n\
+\  compile_rel foo bar\n\
+\)"]; val compile_rel_strongind = DB.fetch "-" "compile_rel_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;; val compile_rel_Var = boolLib.save_thm("compile_rel_Var", Drule.cj 1 compile_rel_rules handle HOL_ERR _ => boolTheory.TRUTH); val compile_rel_Ret = boolLib.save_thm("compile_rel_Ret", Drule.cj 2 compile_rel_rules handle HOL_ERR _ => boolTheory.TRUTH);
 
 (* next_sym reads the next symbol from a string, returning NONE if at eof *)
 val next_sym_def = TotalDefn.qDefine "next_sym_def" [QUOTE " (*#loc 47 25*)\n\
-\     foo = isPREFIX \"(*\" (c::str) "] (SOME (
+\     foo = isPREFIX \"(*\" (c::str)\n\
+\"] (SOME (
   WF_REL_TAC [QUOTE " (*#loc 50 15*)measure (LENGTH o FST) "] THEN REPEAT STRIP_TAC
-));val next_sym_ind = DB.fetch "-" "next_sym_ind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;
+)); val next_sym_ind = DB.fetch "-" "next_sym_ind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;
 
-(Parse.Term [QUOTE " (*#loc 52 4*)f \226\128\185foo\"\226\128\186"])
+(Parse.Term [QUOTE " (*#loc 53 4*)f \226\128\185foo\"\226\128\186"])
 
-val sexpPEG_def = TotalDefn.qDefine "sexpPEG_def" [QUOTE " (*#loc 54 24*)\n\
-\  #\"\\\\\";"
-] NONE; val sexpPEG_ind = DB.fetch "-" "sexpPEG_ind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;
+val sexpPEG_def = TotalDefn.qDefine "sexpPEG_def" [QUOTE " (*#loc 55 24*)\n\
+\  #\"\\\\\";\n\
+\"] NONE; val sexpPEG_ind = DB.fetch "-" "sexpPEG_ind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;
 
-val sexpPEG_start = (fn rule => boolLib.save_thm("sexpPEG_start[simp]",rule)) ( SIMP_CONV(srw_ss())[sexpPEG_def](Parse.Term [QUOTE " (*#loc 58 66*)sexpPEG.start"])
+val sexpPEG_start = boolLib.save_thm("sexpPEG_start[simp]", SIMP_CONV(srw_ss())[sexpPEG_def](Parse.Term [QUOTE " (*#loc 59 66*)sexpPEG.start"])
 
-);val _ = bossLib.Datatype [QUOTE " (*#loc 60 11*) foo = bar"
-];
+);val _ = bossLib.Datatype [QUOTE " (*#loc 61 11*) foo = bar\n\
+\"];
 
-val (reln_rules,reln_ind,reln_cases) = (fn q => fn _ => IndDefLib.xHol_reln "reln" q) [QUOTE "( (*#loc 63 16*)\n\
-\   !x y. x < y ==> reln (x + 1) y) /\\ (\n\
-\\n\
-\   !x y. reln x y ==> reln y x) /\\ (\n\
-\\n\
-\   !x. reln x 0)"
-] NONE; val reln_strongind = DB.fetch "-" "reln_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 3 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
+val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 64 16*)\n\
+\   !x y. x < y ==> reln (x + 1) y\n\
+\) /\\ ( (*#loc 66 5*)\n\
+\   !x y. reln x y ==> reln y x\n\
+\) /\\ ( (*#loc 68 9*)\n\
+\   !x. reln x 0\n\
+\)"]; val reln_strongind = DB.fetch "-" "reln_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;; val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 3 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
 
-val (reln_rules,reln_ind,reln_cases) = (fn q => fn _ => IndDefLib.xHol_reln "reln" q) [QUOTE "( (*#loc 71 16*)\n\
-\ !x y. x < y ==> reln (x + 1) y) /\\ (\n\
-\\n\
+val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 72 16*)\n\
+\ (*#loc 73 10*) !x y. x < y ==> reln (x + 1) y\n\
+\) /\\ ( (*#loc 74 8*)\n\
 \   (!x y. reln x y ==> reln y x) /\\\n\
 \   (!x. reln x 0) /\\\n\
-\   (!y. reln 100 y))"
-] NONE; val reln_strongind = DB.fetch "-" "reln_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;val reln_name1 = boolLib.save_thm("reln_name1", Drule.cj 1 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);val reln_sym = boolLib.save_thm("reln_sym", Drule.cj 2 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
+\   (!y. reln 100 y)\n\
+\)"]; val reln_strongind = DB.fetch "-" "reln_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;; val reln_name1 = boolLib.save_thm("reln_name1", Drule.cj 1 reln_rules handle HOL_ERR _ => boolTheory.TRUTH); val reln_sym = boolLib.save_thm("reln_sym", Drule.cj 2 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
 
-val foo = ba'r[QUOTE " (*#loc 79 18*)\n\
+val foo = ba'r [QUOTE " (*#loc 80 18*)\n\
 \  this is a quotation with\n\
-\ nested \"string\\n\""
-];
+\ nested \"string\\n\"\n\
+\"];
 
-val thmname = (fn rule => boolLib.save_thm("thmname",rule)) ( expression
+val thmname = boolLib.save_thm("thmname", expression
 
-);val _ = bar_x[QUOTE " (*#loc 86 13*)\n\
-\  another quotation (* with unfinished comment \n\
-\  and bare \" with ", ANTIQUOTE(foo),QUOTE " (*#loc 88 23*) and ^"
-];
+);val _ = bar_x [QUOTE " (*#loc 87 13*)\n\
+\  another quotation (* with unfinished comment\n\
+\  and bare \" with ^foo and ^\n\
+\"];
 
-val x = 91 + 10;
+val x = 92 + 10;
 val   y = 11
 val s = ""  
-val s' = "foo.sml" (* #(FNAME) *)
+val s' = "foo.sml" (* #(FILE) *)
diff --git a/tools/Holmake/tests/quote-filter/expected-poly b/tools/Holmake/tests/quote-filter/expected-poly
index 9732158877..9c2fcad688 100644
--- a/tools/Holmake/tests/quote-filter/expected-poly
+++ b/tools/Holmake/tests/quote-filter/expected-poly
@@ -3,12 +3,12 @@
 (Parse.Term [QUOTE " (*#loc 3 3*)\"foo\""])
 [QUOTE " (*#loc 4 2*)foo = #\"^`\""]
 [QUOTE " (*#loc 5 2*)\"\\\"\""]
-(Parse.Term [QUOTE " (*#loc 6 3*)\t"])
+(Parse.Term [QUOTE " (*#loc 6 3*)\009"])
 (Parse.Term [QUOTE " (*#loc 7 3*)(* foo"])
-[QUOTE " (*#loc 8 2*)^"]
+[QUOTE " (*#loc 8 2*)^^"]
 "\"" (Parse.Term [QUOTE " (*#loc 9 8*)foo"])
 "\\" [QUOTE " (*#loc 10 7*)foo"]
-[QUOTE " (*#loc 11 2*)putting unescaped backticks into ", ANTIQUOTE ((antiquotes #"`")),QUOTE " (*#loc 11 53*) is fine"]
+[QUOTE " (*#loc 11 2*)putting unescaped backticks into ", ANTIQUOTE (antiquotes #"`"), QUOTE " (*#loc 11 53*) is fine"]
 (Parse.Term [QUOTE " (*#loc 12 3*)foo\n\
 \bar"])
 (Parse.Term [QUOTE " (*#loc 14 3*)\"an embedded string with \\\n\
@@ -21,74 +21,75 @@
 [QUOTE " (*#loc 21 2*)s1 ^^\n\
 \s2"]
 (* ` *)
-[QUOTE " (*#loc 24 2*)", ANTIQUOTE ((fromMLnum nm)),QUOTE " (*#loc 24 17*) (* *) "];
+[QUOTE " (*#loc 24 2*)", ANTIQUOTE (fromMLnum nm), QUOTE " (*#loc 24 17*) (* *) "];
 (* (*  *) `;*)
 
-val (even_rules,even_ind,even_cases) = (fn q => fn _ => IndDefLib.xHol_reln "even" q) [QUOTE "( (*#loc 27 16*)\n\
-\ even 0) /\\ (\n\
-\ (!n. even n ==> odd (n + 1))) /\\ (\n\
-\\n\
-\  (!m. odd m ==> even (m + 1)))"
-] NONE; val _ = CompilerSpecific.quietbind "val even_strongind = DB.fetch \"-\" \"even_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";val even_0 = boolLib.save_thm("even_0[simp]", Drule.cj 1 even_rules handle HOL_ERR _ => boolTheory.TRUTH);val even_suc = boolLib.save_thm("even_suc", Drule.cj 3 even_rules handle HOL_ERR _ => boolTheory.TRUTH);
+val (even_rules,even_ind,even_cases) = IndDefLib.xHol_reln "even" [QUOTE "( (*#loc 27 16*)\n\
+\ (*#loc 28 12*) even 0\n\
+\) /\\ ( (*#loc 29 5*) (!n. even n ==> odd (n + 1))\n\
+\) /\\ ( (*#loc 30 12*)\n\
+\  (!m. odd m ==> even (m + 1))\n\
+\)"]; val _ = CompilerSpecific.quietbind "val even_strongind = DB.fetch \"-\" \"even_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;"; val even_0 = boolLib.save_thm("even_0[simp]", Drule.cj 1 even_rules handle HOL_ERR _ => boolTheory.TRUTH); val even_suc = boolLib.save_thm("even_suc", Drule.cj 3 even_rules handle HOL_ERR _ => boolTheory.TRUTH);
 
 val foo = TotalDefn.qDefine "foo" [QUOTE " (*#loc 34 16*)\n\
-\  foo x = if x < 2 then 1 else x * foo (x - 1)"
-] NONE; val _ = CompilerSpecific.quietbind "val foo_ind = DB.fetch \"-\" \"foo_ind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";
+\  foo x = if x < 2 then 1 else x * foo (x - 1)\n\
+\"] NONE; val _ = CompilerSpecific.quietbind "val foo_ind = DB.fetch \"-\" \"foo_ind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";
 
-val (compile_rel_rules,compile_rel_ind,compile_rel_cases) = (fn q => fn _ => IndDefLib.xHol_reln "compile_rel" q) [QUOTE "( (*#loc 38 23*)\n\
+val (compile_rel_rules,compile_rel_ind,compile_rel_cases) = IndDefLib.xHol_reln "compile_rel" [QUOTE "( (*#loc 38 23*)\n\
 \  (* (*  *) *)\n\
-\\n\
-\  compile_rel foo bar) /\\ (\n\
-\\n\
-\  compile_rel foo bar)"
-] NONE; val _ = CompilerSpecific.quietbind "val compile_rel_strongind = DB.fetch \"-\" \"compile_rel_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";val compile_rel_Var = boolLib.save_thm("compile_rel_Var", Drule.cj 1 compile_rel_rules handle HOL_ERR _ => boolTheory.TRUTH);val compile_rel_Ret = boolLib.save_thm("compile_rel_Ret", Drule.cj 2 compile_rel_rules handle HOL_ERR _ => boolTheory.TRUTH);
+\ (*#loc 40 8*)\n\
+\  compile_rel foo bar\n\
+\) /\\ ( (*#loc 42 8*)\n\
+\  compile_rel foo bar\n\
+\)"]; val _ = CompilerSpecific.quietbind "val compile_rel_strongind = DB.fetch \"-\" \"compile_rel_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;"; val compile_rel_Var = boolLib.save_thm("compile_rel_Var", Drule.cj 1 compile_rel_rules handle HOL_ERR _ => boolTheory.TRUTH); val compile_rel_Ret = boolLib.save_thm("compile_rel_Ret", Drule.cj 2 compile_rel_rules handle HOL_ERR _ => boolTheory.TRUTH);
 
 (* next_sym reads the next symbol from a string, returning NONE if at eof *)
 val next_sym_def = TotalDefn.qDefine "next_sym_def" [QUOTE " (*#loc 47 25*)\n\
-\     foo = isPREFIX \"(*\" (c::str) "] (SOME (
+\     foo = isPREFIX \"(*\" (c::str)\n\
+\"] (SOME (
   WF_REL_TAC [QUOTE " (*#loc 50 15*)measure (LENGTH o FST) "] THEN REPEAT STRIP_TAC
-));val _ = CompilerSpecific.quietbind "val next_sym_ind = DB.fetch \"-\" \"next_sym_ind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";
+)); val _ = CompilerSpecific.quietbind "val next_sym_ind = DB.fetch \"-\" \"next_sym_ind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";
 
-(Parse.Term [QUOTE " (*#loc 52 4*)f \226\128\185foo\"\226\128\186"])
+(Parse.Term [QUOTE " (*#loc 53 4*)f \226\128\185foo\"\226\128\186"])
 
-val sexpPEG_def = TotalDefn.qDefine "sexpPEG_def" [QUOTE " (*#loc 54 24*)\n\
-\  #\"\\\\\";"
-] NONE; val _ = CompilerSpecific.quietbind "val sexpPEG_ind = DB.fetch \"-\" \"sexpPEG_ind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";
+val sexpPEG_def = TotalDefn.qDefine "sexpPEG_def" [QUOTE " (*#loc 55 24*)\n\
+\  #\"\\\\\";\n\
+\"] NONE; val _ = CompilerSpecific.quietbind "val sexpPEG_ind = DB.fetch \"-\" \"sexpPEG_ind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";
 
-val sexpPEG_start = (fn rule => boolLib.save_thm("sexpPEG_start[simp]",rule)) ( SIMP_CONV(srw_ss())[sexpPEG_def](Parse.Term [QUOTE " (*#loc 58 66*)sexpPEG.start"])
+val sexpPEG_start = boolLib.save_thm("sexpPEG_start[simp]", SIMP_CONV(srw_ss())[sexpPEG_def](Parse.Term [QUOTE " (*#loc 59 66*)sexpPEG.start"])
 
-);val _ = bossLib.Datatype [QUOTE " (*#loc 60 11*) foo = bar"
-];
+);val _ = bossLib.Datatype [QUOTE " (*#loc 61 11*) foo = bar\n\
+\"];
 
-val (reln_rules,reln_ind,reln_cases) = (fn q => fn _ => IndDefLib.xHol_reln "reln" q) [QUOTE "( (*#loc 63 16*)\n\
-\   !x y. x < y ==> reln (x + 1) y) /\\ (\n\
-\\n\
-\   !x y. reln x y ==> reln y x) /\\ (\n\
-\\n\
-\   !x. reln x 0)"
-] NONE; val _ = CompilerSpecific.quietbind "val reln_strongind = DB.fetch \"-\" \"reln_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 3 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
+val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 64 16*)\n\
+\   !x y. x < y ==> reln (x + 1) y\n\
+\) /\\ ( (*#loc 66 5*)\n\
+\   !x y. reln x y ==> reln y x\n\
+\) /\\ ( (*#loc 68 9*)\n\
+\   !x. reln x 0\n\
+\)"]; val _ = CompilerSpecific.quietbind "val reln_strongind = DB.fetch \"-\" \"reln_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;"; val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 3 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
 
-val (reln_rules,reln_ind,reln_cases) = (fn q => fn _ => IndDefLib.xHol_reln "reln" q) [QUOTE "( (*#loc 71 16*)\n\
-\ !x y. x < y ==> reln (x + 1) y) /\\ (\n\
-\\n\
+val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 72 16*)\n\
+\ (*#loc 73 10*) !x y. x < y ==> reln (x + 1) y\n\
+\) /\\ ( (*#loc 74 8*)\n\
 \   (!x y. reln x y ==> reln y x) /\\\n\
 \   (!x. reln x 0) /\\\n\
-\   (!y. reln 100 y))"
-] NONE; val _ = CompilerSpecific.quietbind "val reln_strongind = DB.fetch \"-\" \"reln_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";val reln_name1 = boolLib.save_thm("reln_name1", Drule.cj 1 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);val reln_sym = boolLib.save_thm("reln_sym", Drule.cj 2 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
+\   (!y. reln 100 y)\n\
+\)"]; val _ = CompilerSpecific.quietbind "val reln_strongind = DB.fetch \"-\" \"reln_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;"; val reln_name1 = boolLib.save_thm("reln_name1", Drule.cj 1 reln_rules handle HOL_ERR _ => boolTheory.TRUTH); val reln_sym = boolLib.save_thm("reln_sym", Drule.cj 2 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
 
-val foo = ba'r[QUOTE " (*#loc 79 18*)\n\
+val foo = ba'r [QUOTE " (*#loc 80 18*)\n\
 \  this is a quotation with\n\
-\ nested \"string\\n\""
-];
+\ nested \"string\\n\"\n\
+\"];
 
-val thmname = (fn rule => boolLib.save_thm("thmname",rule)) ( expression
+val thmname = boolLib.save_thm("thmname", expression
 
-);val _ = bar_x[QUOTE " (*#loc 86 13*)\n\
-\  another quotation (* with unfinished comment \n\
-\  and bare \" with ", ANTIQUOTE(foo),QUOTE " (*#loc 88 23*) and ^"
-];
+);val _ = bar_x [QUOTE " (*#loc 87 13*)\n\
+\  another quotation (* with unfinished comment\n\
+\  and bare \" with ^foo and ^\n\
+\"];
 
-val x = 91 + 10;
+val x = 92 + 10;
 val   y = 11
 val s = ""  
-val s' = "foo.sml" (* #(FNAME) *)
+val s' = "foo.sml" (* #(FILE) *)
diff --git a/tools/Holmake/tests/quote-filter/input b/tools/Holmake/tests/quote-filter/input
index 44b4642fa2..28f1c65729 100644
--- a/tools/Holmake/tests/quote-filter/input
+++ b/tools/Holmake/tests/quote-filter/input
@@ -45,7 +45,7 @@ End
 
 (* next_sym reads the next symbol from a string, returning NONE if at eof *)
 Definition next_sym_def:
-     foo = isPREFIX "(*" (c::str) 
+     foo = isPREFIX "(*" (c::str)
 Termination
   WF_REL_TAC `measure (LENGTH o FST) ` THEN REPEAT STRIP_TAC
 End
@@ -85,11 +85,11 @@ End
 Theorem thmname = expression
 
 Quote bar_x:
-  another quotation (* with unfinished comment 
+  another quotation (* with unfinished comment
   and bare " with ^foo and ^
 End
 
 val x = #(LINE) + 10;
 val #(LINE=11) y = #(LINE)
-val s = #(FNAME) #(FNAME=foo.sml)
-val s' = #(FNAME) (* #(FNAME) *)
+val s = #(FILE) #(FILE=foo.sml)
+val s' = #(FILE) (* #(FILE) *)
diff --git a/tools/configure.sml b/tools/configure.sml
index b64977a386..af55ff4589 100644
--- a/tools/configure.sml
+++ b/tools/configure.sml
@@ -304,6 +304,8 @@ val _ =
        systeml (pfx @ extras @ [srcobj])
      end
   in
+    print "Calling mllex on HolLex\n";
+    systeml [mllex, "HolLex"];
     print "Calling mllex on QuoteFilter\n";
     systeml [mllex, "QuoteFilter"];
     compile [] "holpathdb.sig";
@@ -323,12 +325,13 @@ val _ =
     compile [] "Holdep_tokens.sml";
     compile [] "AttributeSyntax.sig";
     compile [] "AttributeSyntax.sml";
+    compile [] "HolLex.sml";
     compile [] "QuoteFilter.sml";
     compile [] "terminal_primitives.sig";
     compile [] "terminal_primitives.sml";
     compile [] "Holmake_tools_dtype.sml";
-    compile [] "QFRead.sig";
-    compile [] "QFRead.sml";
+    compile [] "HolParser.sig";
+    compile [] "HolParser.sml";
     compile ["-I", "mosml"] "Holdep.sig";
     compile ["-I", "mosml"] "Holdep.sml";
     compile [] "Holmake_tools.sig";
@@ -501,30 +504,23 @@ val _ = FileSys.remove (fullPath [holdir, "bin", "buildheap"]) handle _ => ()
 
 val _ = let
   val _ = print "Attempting to compile quote filter ... "
-  val tgt0 = fullPath [holdir, "tools/quote-filter/quote-filter"]
   val tgt = fullPath [holdir, "bin/unquote"]
   val cwd = FileSys.getDir()
-  val _ = FileSys.chDir (fullPath [holdir, "tools/quote-filter"])
-  val _ = systeml [fullPath [holdir, "bin/Holmake"], "cleanAll"]
 in
-  if Process.isSuccess (systeml [fullPath [holdir, "bin/Holmake"]]) then let
-      val instrm = BinIO.openIn tgt0
-      val ostrm = BinIO.openOut tgt
-      val v = BinIO.inputAll instrm
-    in
-      BinIO.output(ostrm, v);
-      BinIO.closeIn instrm;
-      BinIO.closeOut ostrm;
-      mk_xable tgt;
-      print "Quote-filter built\n"
-    end handle e =>
-               (print ("Quote-filter build failed: " ^ General.exnMessage e);
-                OS.Process.exit OS.Process.failure)
-  else (
-    print "Quote-filter build failed\n";
-    OS.Process.exit OS.Process.failure
-  )
-end
+  FileSys.chDir (fullPath [holdir, "tools/quote-filter"]);
+  compile [] "qfilter_util.sig";
+  compile [] "qfilter_util.sml";
+  compile ["-I", holmakedir] "quote-filter.sml";
+  echo "Linking quote-filter.uo";
+  systeml [compiler, "-o", tgt, "-I", holmakedir,
+    "-I", Path.concat(holmakedir, "mosml"),
+    "quote-filter.uo"];
+  mk_xable tgt;
+  print "Quote-filter built\n"
+end handle e => (
+  print ("Quote-filter build failed: " ^ General.exnMessage e);
+  OS.Process.exit OS.Process.failure
+)
 
 (*---------------------------------------------------------------------------
     Configure the muddy library.
diff --git a/tools/mllex/mllex.sml b/tools/mllex/mllex.sml
index b9bad1b24a..fcdea9610a 100644
--- a/tools/mllex/mllex.sml
+++ b/tools/mllex/mllex.sml
@@ -253,6 +253,7 @@ structure LexGen: LEXGEN =
 	  | REPS of int * int | ID of string | ACTION of string
 	  | BOF | EOF | ASSIGN | SEMI | ARROW | LEXMARK | LEXSTATES
 	  | COUNT | REJECT | FULLCHARSET | STRUCT | HEADER | ARG | POSARG
+	  | EOFPOS
 
    datatype exp = EPS | CLASS of bool array * int | CLOSURE of exp
 		| ALT of exp * exp | CAT of exp * exp | TRAIL of int
@@ -271,6 +272,7 @@ structure LexGen: LEXGEN =
 
    val CountNewLines = ref false;
    val PosArg = ref false;
+   val EofPos = ref false;
    val HaveReject = ref false;
 
    (* Can increase size of character set *)
@@ -287,6 +289,7 @@ structure LexGen: LEXGEN =
 
    val ResetFlags = fn () => (CountNewLines := false; HaveReject := false;
 			      PosArg := false;
+			      EofPos := false;
 			      UsesTrailingContext := false;
 			       CharSetSize := 129; StrName := "Mlex";
 				HeaderCode := ""; HeaderDecl:= false;
@@ -516,6 +519,7 @@ fun AdvanceTok () : unit = let
 				  | "header" => HEADER
 				  | "arg"    => ARG
 				  | "posarg" => POSARG
+				  | "eofpos" => EOFPOS
 			          | _ => prErr "unknown % operator "
 			       end
 			     )
@@ -849,6 +853,7 @@ fun parse() : (string * (int list * exp) list * ((string,string) dictionary * st
 				     HeaderDecl := true; ParseDefs())
 				| _ => raise SyntaxError)
 	        | POSARG => (PosArg := true; ParseDefs())
+	        | EOFPOS => (EofPos := true; ParseDefs())
                 | ARG => (LexState := 2; AdvanceTok();
 			     case GetTok()
 			     of ACTION s =>
@@ -1260,7 +1265,8 @@ fun lexGen infile =
 	 sayln "\t\tcase node of";
 	 sayln "\t\t    Internal.N yyk =>";
 	 sayln "\t\t\t(let fun yymktext() = String.substring(!yyb,i0,i-i0)\n\
-	       \\t\t\t     val yypos: int = i0+ !yygone";
+	       \\t\t\t     val yypos: int = i0+ !yygone\n\
+	       \\t\t\t     val yyend: int = yypos + (i-i0)";
 	 if !CountNewLines
 	    then (sayln "\t\t\tval _ = yylineno := CharVectorSlice.foldli";
 	  	  sayln "\t\t\t\t(fn (_,#\"\\n\", n) => n+1 | (_,_, n) => n) (!yylineno) (CharVectorSlice.slice(!yyb,i0,SOME(i-i0)))")
@@ -1289,7 +1295,8 @@ fun lexGen infile =
 	 sayln "\t    in if (String.size newchars)=0";
 	 sayln "\t\t  then (yydone := true;";
 	 say "\t\t        if (l=i0) then UserDeclarations.eof ";
-	 sayln (case !ArgCode of NONE => "()" | SOME _ => "yyarg");
+	 say (case !ArgCode of NONE => "()" | SOME _ => "yyarg");
+	 sayln (if !EofPos then " (!yygone+i0)" else "");
 	 say   "\t\t                  else action(l,NewAcceptingLeaves";
 	 if !UsesTrailingContext then
 	    sayln ",nil))" else sayln "))";
diff --git a/tools/quote-filter/poly-unquote.ML b/tools/quote-filter/poly-unquote.ML
index 41229fe7fa..c12d6dc800 100644
--- a/tools/quote-filter/poly-unquote.ML
+++ b/tools/quote-filter/poly-unquote.ML
@@ -6,7 +6,18 @@ use "../Holmake/Systeml.sig";
 use "../../tools-poly/Holmake/Systeml.sml";
 use "../Holmake/AttributeSyntax.sig";
 use "../Holmake/AttributeSyntax.sml";
+use "../Holmake/HolLex.sml";
 use "../Holmake/QuoteFilter.sml";
+use "../Holmake/HM_SimpleBuffer.sig";
+use "../Holmake/HM_SimpleBuffer.sml";
+use "../Holmake/HOLFS_dtype.sml";
+use "../Holmake/HFS_NameMunge.sig";
+use "../Holmake/poly/HFS_NameMunge.sml";
+use "../Holmake/HOLFS_dtype.sml";
+use "../Holmake/HOLFileSys.sig";
+use "../Holmake/HOLFileSys.sml";
+use "../Holmake/HolParser.sig";
+use "../Holmake/HolParser.sml";
 open OS.Process
 
 fun read_from_stream is n = TextIO.input is;
@@ -19,29 +30,51 @@ fun main() = let
      linked executable as Interrupt exceptions *)
   val _ = Signal.signal(2, Signal.SIG_HANDLE
                                (fn _ => Thread.Thread.broadcastInterrupt()))
-  val {instrm, outstrm, interactive, quotefixp, closefn, infilename} =
-      qfilter_util.processArgs(false,false,false) (CommandLine.arguments())
+  val {instrm, outstrm, interactive, quotefixp, oldparser, closefn, infilename} =
+      qfilter_util.processArgs(false,false,false,false) (CommandLine.arguments())
 
 (* with many thanks to Ken Friis Larsen, Peter Sestoft, Claudio Russo and
    Kenn Heinrich who helped me see the light with respect to this code *)
 
-  open QuoteFilter.UserDeclarations
-  val state as QFS args = newstate {inscriptp = interactive,
-                                    quotefixp = quotefixp,
-                                    scriptfilename = infilename}
-
-  fun loop() =
-    let
-      val lexer = #2 o QuoteFilter.makeLexer (read_from_stream instrm) state
-      fun coreloop () =
-        case lexer() of
-            "" => ()
-          | s => (TextIO.output(outstrm, s); coreloop())
-    in
-      coreloop() handle Interrupt => (resetstate state; loop())
-    end
+  val loop =
+    if oldparser orelse quotefixp then let
+      open QuoteFilter.UserDeclarations
+      val state as QFS args = newstate {inscriptp = interactive,
+                                        quotefixp = quotefixp,
+                                        scriptfilename = infilename}
+
+      fun loop() =
+        let
+          val lexer = #2 o QuoteFilter.makeLexer (read_from_stream instrm) state
+          fun coreloop () =
+            case lexer() of
+                "" => ()
+              | s => (TextIO.output(outstrm, s); coreloop())
+        in
+          coreloop() handle Interrupt => (resetstate state; loop())
+        end
+      in loop end
+    else let
+      open HolParser.ToSML
+      val read = mkPushTranslator {
+        read = read_from_stream instrm,
+        filename = infilename,
+        parseError = fn (start, stop) => fn s =>
+          TextIO.output (TextIO.stdErr,
+            "parse error at " ^ Int.toString start ^ "-" ^ Int.toString stop ^ ": " ^ s ^ "\n")
+      } (mkStrcode (fn s => TextIO.output(outstrm, s)))
+
+      fun loop () = if read () then () else loop ()
+      in loop end
 in
   loop();
   closefn();
   exit success
-end;
+end handle e => (
+  TextIO.output (TextIO.stdErr, "Uncaught exception" ^
+    (case PolyML.Exception.exceptionLocation e of
+        NONE => ""
+      | SOME {file, startLine, ...} => " at " ^ file ^ ":" ^ FixedInt.toString startLine) ^
+    ": " ^ General.exnMessage e);
+  PolyML.Exception.reraise e
+);
diff --git a/tools/quote-filter/qfilter_util.sig b/tools/quote-filter/qfilter_util.sig
index 531aa1c8f3..b2dfaeb67f 100644
--- a/tools/quote-filter/qfilter_util.sig
+++ b/tools/quote-filter/qfilter_util.sig
@@ -1,13 +1,14 @@
 signature qfilter_util =
 sig
 
-  val processArgs : bool * bool * bool -> string list ->
+  val processArgs : bool * bool * bool * bool -> string list ->
                     {instrm: TextIO.instream,
-                     outstrm : TextIO.outstream,
+                     outstrm: TextIO.outstream,
                      interactive: bool,
-                     quotefixp : bool,
-                     closefn : unit -> unit,
-                     infilename : string
+                     quotefixp: bool,
+                     oldparser: bool,
+                     closefn: unit -> unit,
+                     infilename: string
                     }
 
 end
diff --git a/tools/quote-filter/qfilter_util.sml b/tools/quote-filter/qfilter_util.sml
index a592f17a57..bc5f478208 100644
--- a/tools/quote-filter/qfilter_util.sml
+++ b/tools/quote-filter/qfilter_util.sml
@@ -3,7 +3,7 @@ struct
 
 open OS.Process
 fun nothing() = ()
-fun open_files intp infn outfn =
+fun open_files intp oldp infn outfn =
     let
       open TextIO
       val is = TextIO.openIn infn
@@ -33,7 +33,7 @@ fun open_files intp infn outfn =
           end
     in
       {instrm = is, outstrm = os, interactive = intp, quotefixp = false,
-       closefn = cb, infilename = infn}
+       oldparser = oldp, closefn = cb, infilename = infn}
     end
 
 fun usage strm status =
@@ -46,11 +46,12 @@ fun usage strm status =
                    \Other options occur as sole arguments:\n\
                    \   -h : show this message\n\
                    \   -n : don't use \"interactive\" mode\n\
+                   \   -q : use old \"QuoteFilter\" parser\n\
                    \   --quotefix : filter to replace ` with Unicode quotes\n");
      exit status)
 
 fun badusage() = usage TextIO.stdErr failure
-fun processArgs (nonp, intp, qfixp) args =
+fun processArgs (nonp, intp, qfixp, oldp) args =
     case args of
         [] => if intp then badusage()
               else if qfixp then
@@ -58,6 +59,7 @@ fun processArgs (nonp, intp, qfixp) args =
                  outstrm = TextIO.stdOut,
                  interactive = false,
                  quotefixp = qfixp,
+                 oldparser = oldp,
                  closefn = nothing,
                  infilename = ""}
               else
@@ -65,20 +67,22 @@ fun processArgs (nonp, intp, qfixp) args =
                  outstrm = TextIO.stdOut,
                  interactive = true,
                  quotefixp = false,
+                 oldparser = oldp,
                  closefn = nothing,
                  infilename = ""}
       | ["-h"] => usage TextIO.stdOut success
       | "-h" :: _ => badusage()
       | "-i" :: rest => if nonp orelse qfixp then badusage()
-                        else processArgs (false, true, false) rest
+                        else processArgs (false, true, false, oldp) rest
       | "-n"::rest =>
            if intp orelse qfixp then badusage()
-           else processArgs (true, false, false) rest
+           else processArgs (true, false, false, oldp) rest
+      | "-q"::rest => processArgs (nonp, intp, qfixp, true) rest
       | "--quotefix"::rest =>
            if intp orelse nonp then badusage()
-           else processArgs (false, false, true) rest
+           else processArgs (false, false, true, oldp) rest
       | [ifile, ofile] => if qfixp orelse nonp then badusage()
-                          else open_files intp ifile ofile
+                          else open_files intp oldp ifile ofile
       | _ => badusage()
 
 end (* struct *)
diff --git a/tools/quote-filter/quote-filter.sml b/tools/quote-filter/quote-filter.sml
index 1ac2e1b08e..dec9aa213a 100644
--- a/tools/quote-filter/quote-filter.sml
+++ b/tools/quote-filter/quote-filter.sml
@@ -7,28 +7,41 @@ val _ = catch_interrupt true;
 
 fun read_from_stream is n = TextIO.input is
 
-val {instrm=instream, outstrm = outstream, interactive = intp,
-     quotefixp = qfixp, closefn = callback, infilename} =
-    processArgs (false,false,false) (CommandLine.arguments())
-
-open QuoteFilter.UserDeclarations
-val state as QFS args = newstate {inscriptp = intp, quotefixp = qfixp,
-                                  scriptfilename = infilename}
-
+val {instrm = instream, outstrm = outstream, interactive = intp,
+     quotefixp = qfixp, oldparser = oldp, closefn = callback, infilename} =
+    processArgs (false,false,false,false) (CommandLine.arguments())
 
 (* with many thanks to Ken Friis Larsen, Peter Sestoft, Claudio Russo and
    Kenn Heinrich who helped me see the light with respect to this code *)
-fun loop() =
-  let
-    val lexer = #2 o QuoteFilter.makeLexer (read_from_stream instream) state
-    fun coreloop () =
-      case lexer() of
-          "" => ()
-        | s => (TextIO.output(outstream, s); TextIO.flushOut outstream;
-                coreloop())
-  in
-    coreloop() handle Interrupt => (resetstate state; loop())
-  end
+val loop =
+  if oldp orelse qfixp then let
+    open QuoteFilter.UserDeclarations
+    val state as QFS args = newstate {inscriptp = intp, quotefixp = qfixp,
+                                      scriptfilename = infilename}
+
+    fun loop() =
+      let
+        val lexer = #2 o QuoteFilter.makeLexer (read_from_stream instream) state
+        fun coreloop () =
+          case lexer() of
+              "" => ()
+            | s => (TextIO.output(outstream, s); coreloop())
+      in
+        coreloop() handle Interrupt => (resetstate state; loop())
+      end
+    in loop end
+  else let
+    open HolParser.ToSML
+    val read = mkPushTranslator {
+      read = read_from_stream instream,
+      filename = infilename,
+      parseError = fn (start, stop) => fn s =>
+        TextIO.output (TextIO.stdErr,
+          "parse error at " ^ Int.toString start ^ "-" ^ Int.toString stop ^ ": " ^ s ^ "\n")
+    } (mkStrcode (fn s => TextIO.output(outstream, s)))
+
+    fun loop () = if read () then () else loop ()
+    in loop end
 
 val _ = loop()
 val _ = callback()