# HG changeset patch
# User blanchet
# Date 1300985367 -3600
# Node ID 447fa058ab222c1ce906dbe34c3dddcabf961568
# Parent  f978caf60bbe675e0a652980d7170206c03b8965
avoid evil "export_without_context", which breaks if there are local "fixes"

diff -r f978caf60bbe -r 447fa058ab22 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Mar 24 17:49:27 2011 +0100
@@ -9,6 +9,7 @@
 sig
   val new_skolem_var_prefix : string
   val new_nonskolem_var_prefix : string
+  val is_zapped_var_name : string -> bool
   val extensionalize_theorem : thm -> thm
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
@@ -27,6 +28,10 @@
 val new_skolem_var_prefix = "MesonSK"
 val new_nonskolem_var_prefix = "MesonV"
 
+fun is_zapped_var_name s =
+  exists (fn prefix => String.isPrefix prefix s)
+         [new_skolem_var_prefix, new_nonskolem_var_prefix]
+
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
 val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
@@ -328,13 +333,20 @@
         val no_choice = null choice_ths
         val discharger_th =
           th |> (if no_choice then pull_out else skolemize choice_ths)
-        val fully_skolemized_t =
+        val zapped_th =
           discharger_th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
           |> (if no_choice then
                 Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> cprop_of
               else
                 cterm_of thy)
-          |> zap true |> Drule.export_without_context
+          |> zap true
+        val fixes =
+          Term.add_free_names (prop_of zapped_th) []
+          |> filter is_zapped_var_name
+        val ctxt' = ctxt |> Variable.add_fixes_direct fixes (*###*)
+        val fully_skolemized_t =
+          zapped_th
+          |> singleton (Variable.export ctxt' ctxt)
           |> cprop_of |> Thm.dest_equals |> snd |> term_of
       in
         if exists_subterm (fn Var ((s, _), _) =>
diff -r f978caf60bbe -r 447fa058ab22 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Mar 24 17:49:27 2011 +0100
@@ -38,10 +38,6 @@
 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 [] = []
@@ -619,7 +615,7 @@
     fun unify_potential_flex comb atom =
       if is_flex comb then unify_flex comb atom
       else if is_Var atom then add_terms (atom, comb)
-      else raise TERM ("unify_terms", [comb, atom])
+      else raise TERM ("unify_potential_flex", [comb, atom])
     fun unify_terms (t, u) =
       case (t, u) of
         (t1 $ t2, u1 $ u2) =>
@@ -662,7 +658,7 @@
     fun do_instantiate th =
       let
         val var = Term.add_vars (prop_of th) []
-                  |> filter (is_zapped_var_name o fst o fst)
+                  |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
                   |> the_single
       in th |> term_instantiate thy [(Var var, t')] end
   in
@@ -751,7 +747,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)
+                 |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
                  |> sort (cluster_ord
                           o pairself (Meson_Clausify.cluster_of_zapped_var_name
                                       o fst o fst))
@@ -801,7 +797,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)
+           |> filter (Meson_Clausify.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)
@@ -837,7 +833,7 @@
               THEN ALLGOALS (fn i =>
                        rtac @{thm Meson.skolem_COMBK_I} i
                        THEN rotate_tac (rotation_for_subgoal i) i
-(*                       THEN PRIMITIVE (unify_first_prem_with_concl thy i) ### FIXME: needed? *)
+(*                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)  FIXME: needed? *)
                        THEN assume_tac i)))
       handle ERROR _ =>
              error ("Cannot replay Metis proof in Isabelle:\n\