more robust handling of variables in new Skolemizer

--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Mar 24 17:10:23 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Mar 24 17:49:27 2011 +0100
@@ -8,6 +8,7 @@
 signature MESON_CLAUSIFY =
 sig
   val new_skolem_var_prefix : string
+  val new_nonskolem_var_prefix : string
   val extensionalize_theorem : thm -> thm
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Mar 24 17:10:23 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Mar 24 17:49:27 2011 +0100
@@ -38,6 +38,10 @@
 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 [] = []
@@ -46,7 +50,7 @@
 
 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
@@ -656,9 +660,11 @@
       | 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
@@ -745,6 +751,7 @@
             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))
@@ -762,15 +769,13 @@
         | _ => 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) =
@@ -796,6 +801,7 @@
                      \\"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)

--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu Mar 24 17:10:23 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu Mar 24 17:49:27 2011 +0100
@@ -36,6 +36,7 @@
      tfrees: type_literal list,
      old_skolems: (string * term) list}
 
+  val metis_generated_var_prefix : string
   val type_tag_name : string
   val bound_var_prefix : string
   val schematic_var_prefix: string
@@ -83,6 +84,8 @@
 structure Metis_Translate : METIS_TRANSLATE =
 struct
 
+val metis_generated_var_prefix = "_"
+
 val type_tag_name = "ti"
 
 val bound_var_prefix = "B_"