src/HOL/Tools/Metis/metis_reconstruct.ML

   val trace : bool Config.T
   val trace_msg : Proof.context -> (unit -> string) -> unit
   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
+    Proof.context -> mode -> (string * term) list * int Unsynchronized.ref
     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
     -> (Metis_Thm.thm * thm) list
   val discharge_skolem_premises :
     Proof.context -> (thm * term) option list -> thm -> thm
   val setup : theory -> theory

       case strip_prefix_and_unascii tfree_prefix x of
           SOME tf => mk_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 =
+fun hol_term_from_metis_PT ctxt new_skolem_var_count fol_tm =
   let val thy = ProofContext.theory_of ctxt
       val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
                                        Metis_Term.toString fol_tm)
       fun tm_to_tt (Metis_Term.Var v) =
              (case strip_prefix_and_unascii tvar_prefix v of

                     val c = smart_invert_const b
                     val ntypes = num_type_args thy c
                     val nterms = length ts - ntypes
                     val tts = map tm_to_tt ts
                     val tys = types_of (List.take(tts,ntypes))
+                    val j = !new_skolem_var_count + 1
+                    val _ = new_skolem_var_count := j
                     val t =
                       if String.isPrefix new_skolem_const_prefix c then
-                        Var (new_skolem_var_from_const c,
+                        Var ((new_skolem_var_name_from_const c, j),
                              Type_Infer.paramify_vars (tl tys ---> hd tys))
                       else
                         Const (c, dummyT)
                   in if length tys = ntypes then
                          apply_list t nterms (List.drop(tts,ntypes))

       SomeTerm t => t
     | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
   end
 
 (*Maps fully-typed metis terms to isabelle terms*)
-fun hol_term_from_metis_FT ctxt fol_tm =
+fun hol_term_from_metis_FT ctxt new_skolem_var_count fol_tm =
   let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
                                        Metis_Term.toString fol_tm)
       fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
              (case strip_prefix_and_unascii schematic_var_prefix v of
                   SOME w =>  mk_var(w, dummyT)

               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix_and_unascii fixed_var_prefix x of
                 SOME v => Free (v, dummyT)
               | NONE => (trace_msg ctxt (fn () =>
                                       "hol_term_from_metis_FT bad const: " ^ x);
-                         hol_term_from_metis_PT ctxt t))
+                         hol_term_from_metis_PT ctxt new_skolem_var_count t))
         | cvt t = (trace_msg ctxt (fn () =>
                    "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
-                   hol_term_from_metis_PT ctxt t)
+                   hol_term_from_metis_PT ctxt new_skolem_var_count t)
   in fol_tm |> cvt end
 
 fun hol_term_from_metis FT = hol_term_from_metis_FT
   | hol_term_from_metis _ = hol_term_from_metis_PT
 
-fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
-  let val ts = map (hol_term_from_metis mode ctxt) fol_tms
+fun hol_terms_from_metis ctxt mode (old_skolems, new_skolem_var_count) fol_tms =
+  let val ts = map (hol_term_from_metis mode ctxt new_skolem_var_count) 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

   let val th = EXCLUDED_MIDDLE
       val [vx] = Term.add_vars (prop_of th) []
       val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   in  cterm_instantiate substs th  end;
 
-fun assume_inf ctxt mode old_skolems atm =
+fun assume_inf ctxt mode skolem_params atm =
   inst_excluded_middle
       (ProofContext.theory_of ctxt)
-      (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm))
+      (singleton (hol_terms_from_metis ctxt mode skolem_params)
+                 (Metis_Term.Fn atm))
 
 (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
    to reconstruct them admits new possibilities of errors, e.g. concerning
    sorts. Instead we try to arrange that new TVars are distinct and that types
    can be inferred from terms. *)
 
-fun inst_inf ctxt mode old_skolems thpairs fsubst th =
+fun inst_inf ctxt mode (old_skolems, new_skolem_var_count) thpairs fsubst th =
   let val thy = ProofContext.theory_of ctxt
       val i_th = lookth thpairs th
       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 ctxt y
+            val t = hol_term_from_metis mode ctxt new_skolem_var_count 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)

 val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection]
 
 (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
 val select_literal = negate_head oo make_last
 
-fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
+fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
   let
     val thy = ProofContext.theory_of ctxt
     val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
     val _ = trace_msg ctxt (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
     val _ = trace_msg ctxt (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)

     else if Thm.eq_thm (TrueI, i_th2) then
       i_th1
     else
       let
         val i_atm =
-          singleton (hol_terms_from_fol ctxt mode old_skolems)
+          singleton (hol_terms_from_metis ctxt mode skolem_params)
                     (Metis_Term.Fn atm)
         val _ = trace_msg ctxt (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
         val prems_th1 = prems_of i_th1
         val prems_th2 = prems_of i_th2
         val index_th1 =

 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
 
 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
 
-fun refl_inf ctxt mode old_skolems t =
+fun refl_inf ctxt mode skolem_params t =
   let val thy = ProofContext.theory_of ctxt
-      val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
+      val i_t = singleton (hol_terms_from_metis ctxt mode skolem_params) t
       val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
       val c_t = cterm_incr_types thy refl_idx i_t
   in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
 
 (* INFERENCE RULE: EQUALITY *)

 
 fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0  (*equality has no type arguments*)
   | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
   | get_ty_arg_size _ _ = 0;
 
-fun equality_inf ctxt mode old_skolems (pos, atm) fp fr =
+fun equality_inf ctxt mode skolem_params (pos, atm) fp fr =
   let val thy = ProofContext.theory_of ctxt
       val m_tm = Metis_Term.Fn atm
-      val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
+      val [i_atm,i_tm] = hol_terms_from_metis ctxt mode skolem_params [m_tm, fr]
       val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
       fun replace_item_list lx 0 (_::ls) = lx::ls
         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
       fun path_finder_FO tm [] = (tm, Bound 0)
         | path_finder_FO tm (p::ps) =

         (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   in  cterm_instantiate eq_terms subst'  end;
 
 val factor = Seq.hd o distinct_subgoals_tac;
 
-fun step ctxt mode old_skolems thpairs p =
+fun step ctxt mode skolem_params thpairs p =
   case p of
     (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
-  | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm
+  | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolem_params f_atm
   | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
-    factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
+    factor (inst_inf ctxt mode skolem_params thpairs f_subst f_th1)
   | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
-    factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
-  | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
+    factor (resolve_inf ctxt mode skolem_params thpairs f_atm f_th1 f_th2)
+  | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolem_params f_tm
   | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
-    equality_inf ctxt mode old_skolems f_lit f_p f_r
+    equality_inf ctxt mode skolem_params f_lit f_p f_r
 
 fun flexflex_first_order th =
   case Thm.tpairs_of th of
       [] => th
     | pairs =>

 fun is_isabelle_literal_genuine t =
   case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
 
 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
 
-fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
+fun replay_one_inference ctxt mode skolem_params (fol_th, inf) thpairs =
   let
     val _ = trace_msg ctxt (fn () => "=============================================")
     val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
     val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
-    val th = step ctxt mode old_skolems thpairs (fol_th, inf)
+    val th = step ctxt mode skolem_params thpairs (fol_th, inf)
              |> flexflex_first_order
     val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
     val _ = trace_msg ctxt (fn () => "=============================================")
     val num_metis_lits =
       fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList