# 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.")