# HG changeset patch
# User blanchet
# Date 1302171386 -7200
# Node ID 5f2960582e45fef2649daba4d4f8b8433c62d2f8
# Parent  554e90f9db0ca37732a6c53ee602f7acbd0213e0
make new Skolemizer more robust

diff -r 554e90f9db0c -r 5f2960582e45 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 07 12:16:25 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 07 12:16:26 2011 +0200
@@ -105,7 +105,7 @@
                 | 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)) )
+                | NONE   => SomeTerm (mk_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 (".",_)) =
@@ -612,10 +612,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
+      case Term.add_vars (prop_of th) []
+           |> filter_out (Meson_Clausify.is_zapped_var_name o fst o fst) of
+        [] => th
+      | [var] => th |> term_instantiate thy [(Var var, t')]
+      | _ => raise Fail "expected a single non-zapped Var"
   in
     (etac @{thm allE} i
      THEN rotate_tac ~1 i
@@ -753,7 +754,7 @@
                     Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
                                                   (Integer.add 1)) substs
         |> Int_Tysubst_Table.dest
-(* for debugging:
+(* for debugging only:
       fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
         "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
         "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
@@ -778,7 +779,8 @@
               THEN ALLGOALS (fn i =>
                        rtac @{thm Meson.skolem_COMBK_I} i
                        THEN rotate_tac (rotation_for_subgoal i) i
-                       THEN assume_tac i)))
+                       THEN assume_tac 1
+                       THEN flexflex_tac)))
       handle ERROR _ =>
              error ("Cannot replay Metis proof in Isabelle:\n\
                     \Error when discharging Skolem assumptions.")