src/HOL/Tools/Metis/metis_reconstruct.ML

   val trace : bool Config.T
   val trace_msg : Proof.context -> (unit -> string) -> unit
   val verbose : bool Config.T
   val verbose_warning : Proof.context -> string -> unit
   val hol_term_from_metis :
-    mode -> int Symtab.table -> Proof.context -> Metis_Term.term -> term
+    Proof.context -> mode -> int Symtab.table -> Metis_Term.term -> term
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   val untyped_aconv : term * term -> bool
   val replay_one_inference :
     Proof.context -> mode -> (string * term) list -> int Symtab.table
     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list

 fun terms_of [] = []
   | terms_of (SomeTerm t :: tts) = t :: terms_of tts
   | terms_of (SomeType _ :: tts) = terms_of tts;
 
 fun types_of [] = []
-  | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
-      if String.isPrefix metis_generated_var_prefix a then
-          (*Variable generated by Metis, which might have been a type variable.*)
-          TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
-      else types_of tts
+  | types_of (SomeTerm (Var ((a, idx), _)) :: tts) =
+    types_of tts
+    |> (if String.isPrefix metis_generated_var_prefix a then
+          (* Variable generated by Metis, which might have been a type
+             variable. *)
+          cons (TVar (("'" ^ a, idx), HOLogic.typeS))
+        else
+          I)
   | types_of (SomeTerm _ :: tts) = types_of tts
-  | types_of (SomeType T :: tts) = T :: types_of tts;
+  | types_of (SomeType T :: tts) = T :: types_of tts
 
 fun apply_list rator nargs rands =
   let val trands = terms_of rands
   in  if length trands = nargs then SomeTerm (list_comb(rator, trands))
       else raise Fail

   Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt);
 
 (* We use 1 rather than 0 because variable references in clauses may otherwise
    conflict with variable constraints in the goal...at least, type inference
    often fails otherwise. See also "axiom_inf" below. *)
-fun mk_var (w, T) = Var ((w, 1), T)
-
-(*include the default sort, if available*)
-fun mk_tfree ctxt w =
-  let val ww = "'" ^ w
-  in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
+fun make_var (w, T) = Var ((w, 1), T)
 
 (*Remove the "apply" operator from an HO term*)
 fun strip_happ args (Metis_Term.Fn (".", [t, u])) = strip_happ (u :: args) t
   | strip_happ args x = (x, args)
-
-fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
 
 fun hol_type_from_metis_term _ (Metis_Term.Var v) =
      (case strip_prefix_and_unascii tvar_prefix v of
           SOME w => make_tvar w
         | NONE   => make_tvar v)

      (case strip_prefix_and_unascii type_const_prefix x of
           SOME tc => Type (invert_const tc,
                            map (hol_type_from_metis_term ctxt) tys)
         | NONE    =>
       case strip_prefix_and_unascii tfree_prefix x of
-          SOME tf => mk_tfree ctxt tf
+          SOME tf => make_tfree ctxt tf
         | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
 
 (*Maps metis terms to isabelle terms*)
 fun hol_term_from_metis_PT ctxt fol_tm =
   let val thy = Proof_Context.theory_of ctxt

       fun tm_to_tt (Metis_Term.Var v) =
              (case strip_prefix_and_unascii tvar_prefix v of
                   SOME w => SomeType (make_tvar w)
                 | NONE =>
               case strip_prefix_and_unascii schematic_var_prefix v of
-                  SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
-                | NONE   => SomeTerm (mk_var (v, HOLogic.typeT)))
+                  SOME w => SomeTerm (make_var (w, HOLogic.typeT))
+                | NONE   => SomeTerm (make_var (v, HOLogic.typeT)))
                     (*Var from Metis with a name like _nnn; possibly a type variable*)
         | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
         | tm_to_tt (t as Metis_Term.Fn (".", _)) =
             let val (rator,rands) = strip_happ [] t in
               case rator of

             case strip_prefix_and_unascii type_const_prefix a of
                 SOME b =>
                 SomeType (Type (invert_const b, types_of (map tm_to_tt ts)))
               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
             case strip_prefix_and_unascii tfree_prefix a of
-                SOME b => SomeType (mk_tfree ctxt b)
+                SOME b => SomeType (make_tfree ctxt b)
               | NONE => (*a fixed variable? They are Skolem functions.*)
             case strip_prefix_and_unascii fixed_var_prefix a of
                 SOME b =>
                   let val opr = Free (b, HOLogic.typeT)
                   in  apply_list opr (length ts) (map tm_to_tt ts)  end

           else
             Const (c, dummyT)
         end
       fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) =
              (case strip_prefix_and_unascii schematic_var_prefix v of
-                  SOME w =>  mk_var(w, dummyT)
-                | NONE   => mk_var(v, dummyT))
+                  SOME w =>  make_var (w, dummyT)
+                | NONE   => make_var (v, dummyT))
         | cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) =
             Const (@{const_name HOL.eq}, HOLogic.typeT)
         | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) =
            (case strip_prefix_and_unascii const_prefix x of
                 SOME c => do_const c

     let val (s, swap) = atp_name_from_metis s in
       ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
     end
   | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
 
-fun hol_term_from_metis_MX sym_tab ctxt =
-  let val thy = Proof_Context.theory_of ctxt in
-    atp_term_from_metis #> term_from_atp thy false sym_tab []
-    (* FIXME ### tfrees instead of []? *) NONE
-  end
-
-fun hol_term_from_metis FO _ = hol_term_from_metis_PT
-  | hol_term_from_metis HO _ = hol_term_from_metis_PT
-  | hol_term_from_metis FT _ = hol_term_from_metis_FT
-  | hol_term_from_metis MX sym_tab = hol_term_from_metis_MX sym_tab
+fun hol_term_from_metis_MX ctxt sym_tab =
+  atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
+
+fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt
+  | hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt
+  | hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt
+  | hol_term_from_metis ctxt MX sym_tab = hol_term_from_metis_MX ctxt sym_tab
 
 fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
-  let val ts = map (hol_term_from_metis mode sym_tab ctxt) fol_tms
+  let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms
       val _ = trace_msg ctxt (fn () => "  calling type inference:")
       val _ = app (fn t => trace_msg ctxt
                                      (fn () => Syntax.string_of_term ctxt t)) ts
       val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
                    |> infer_types ctxt

 
 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
 
 (* INFERENCE RULE: AXIOM *)
 
-(* This causes variables to have an index of 1 by default. See also "mk_var"
+(* This causes variables to have an index of 1 by default. See also "make_var"
    above. *)
 fun axiom_inf th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th)
 
 (* INFERENCE RULE: ASSUME *)
 

       val i_th_vars = Term.add_vars (prop_of i_th) []
       fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
       fun subst_translation (x,y) =
         let val v = find_var x
             (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
-            val t = hol_term_from_metis mode sym_tab ctxt y
+            val t = hol_term_from_metis ctxt mode sym_tab y
         in  SOME (cterm_of thy (Var v), t)  end
         handle Option.Option =>
                (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
                                          " in " ^ Display.string_of_thm ctxt i_th);
                 NONE)

 
 (* INFERENCE RULE: RESOLVE *)
 
 (* Like RSN, but we rename apart only the type variables. Vars here typically
    have an index of 1, and the use of RSN would increase this typically to 3.
-   Instantiations of those Vars could then fail. See comment on "mk_var". *)
+   Instantiations of those Vars could then fail. See comment on "make_var". *)
 fun resolve_inc_tyvars thy tha i thb =
   let
     val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
     fun aux tha thb =
       case Thm.bicompose false (false, tha, nprems_of tha) i thb