src/HOL/Tools/Metis/metis_reconstruct.ML

 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 fun verbose_warning ctxt msg =
   if Config.get ctxt verbose then warning msg else ()
 
+val is_zapped_var_name =
+  String.isPrefix Meson_Clausify.new_skolem_var_prefix orf
+  String.isPrefix Meson_Clausify.new_nonskolem_var_prefix
+
 datatype term_or_type = SomeTerm of term | SomeType of typ
 
 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 "_" a then
+      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 _ :: tts) = types_of tts
   | types_of (SomeType T :: tts) = T :: types_of tts;

            if k > j then t else t $ u
          | (t, u) => t $ u)
       | repair t = t
     val t' = t |> repair |> fold (curry absdummy) (map snd params)
     fun do_instantiate th =
-      let val var = Term.add_vars (prop_of th) [] |> the_single in
-        th |> term_instantiate thy [(Var var, t')]
-      end
+      let
+        val var = Term.add_vars (prop_of th) []
+                  |> filter (is_zapped_var_name o fst o fst)
+                  |> the_single
+      in th |> term_instantiate thy [(Var var, t')] end
   in
     (etac @{thm allE} i
      THEN rotate_tac ~1 i
      THEN PRIMITIVE do_instantiate) st
   end

         let
           val (tyenv, tenv) =
             Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
           val tsubst =
             tenv |> Vartab.dest
+                 |> filter (is_zapped_var_name o fst o fst)
                  |> sort (cluster_ord
                           o pairself (Meson_Clausify.cluster_of_zapped_var_name
                                       o fst o fst))
                  |> map (Meson.term_pair_of
                          #> pairself (Envir.subst_term_types tyenv))

                      match_term (nth axioms ax_no |> the |> snd, t)))
           end
         | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
                            [prem])
       fun cluster_of_var_name skolem s =
-        let
-          val ((ax_no, (cluster_no, _)), skolem') =
-            Meson_Clausify.cluster_of_zapped_var_name s
-        in
+        case try Meson_Clausify.cluster_of_zapped_var_name s of
+          NONE => NONE
+        | SOME ((ax_no, (cluster_no, _)), skolem') =>
           if skolem' = skolem andalso cluster_no > 0 then
             SOME (ax_no, cluster_no)
           else
             NONE
-        end
       fun clusters_in_term skolem t =
         Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
       fun deps_for_term_subst (var, t) =
         case clusters_in_term false var of
           [] => NONE

         handle Int_Pair_Graph.CYCLES _ =>
                error "Cannot replay Metis proof in Isabelle without \
                      \\"Hilbert_Choice\"."
       val outer_param_names =
         [] |> fold (Term.add_var_names o snd) (map_filter I axioms)
+           |> filter (is_zapped_var_name o fst)
            |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
            |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
                          cluster_no = 0 andalso skolem)
            |> sort shuffle_ord |> map (fst o snd)
       val ax_counts =