--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Oct 26 11:23:27 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Oct 26 11:31:03 2010 +0200
@@ -754,8 +754,8 @@
|> fold Int_Pair_Graph.add_deps_acyclic depss
|> Int_Pair_Graph.topological_order
handle Int_Pair_Graph.CYCLES _ =>
- error "Cannot replay Metis proof in Isabelle without axiom of \
- \choice."
+ error "Cannot replay Metis proof in Isabelle without \
+ \\"Hilbert_Choice\"."
val params0 =
[] |> fold (Term.add_vars o snd) (map_filter I axioms)
|> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst))
@@ -796,6 +796,9 @@
THEN rotate_tac (rotation_for_subgoal i) i
(* THEN PRIMITIVE (unify_first_prem_with_concl thy i) ###*)
THEN assume_tac i)))
+ handle ERROR _ =>
+ error ("Cannot replay Metis proof in Isabelle:\n\
+ \Error when discharging Skolem assumptions.")
end
val setup = trace_setup
--- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Oct 26 11:23:27 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Oct 26 11:31:03 2010 +0200
@@ -70,7 +70,7 @@
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss
val (mode, {axioms, tfrees, old_skolems}) =
- build_logic_map mode ctxt type_lits cls thss
+ prepare_metis_problem mode ctxt type_lits cls thss
val _ = if null tfrees then ()
else (trace_msg ctxt (fn () => "TFREE CLAUSES");
app (fn TyLitFree ((s, _), (s', _)) =>
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Oct 26 11:23:27 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Oct 26 11:31:03 2010 +0200
@@ -31,7 +31,7 @@
datatype fol_literal = FOLLiteral of bool * combterm
datatype mode = FO | HO | FT
- type logic_map =
+ type metis_problem =
{axioms: (Metis_Thm.thm * thm) list,
tfrees: type_literal list,
old_skolems: (string * term) list}
@@ -74,9 +74,9 @@
val tvar_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
val string_of_mode : mode -> string
- val build_logic_map :
+ val prepare_metis_problem :
mode -> Proof.context -> bool -> thm list -> thm list list
- -> mode * logic_map
+ -> mode * metis_problem
end
structure Metis_Translate : METIS_TRANSLATE =
@@ -662,7 +662,7 @@
(* Logic maps manage the interface between HOL and first-order logic. *)
(* ------------------------------------------------------------------------- *)
-type logic_map =
+type metis_problem =
{axioms: (Metis_Thm.thm * thm) list,
tfrees: type_literal list,
old_skolems: (string * term) list}
@@ -678,7 +678,7 @@
end;
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
-fun add_tfrees {axioms, tfrees, old_skolems} : logic_map =
+fun add_tfrees {axioms, tfrees, old_skolems} : metis_problem =
{axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
axioms,
tfrees = tfrees, old_skolems = old_skolems}
@@ -722,7 +722,7 @@
end;
(* Function to generate metis clauses, including comb and type clauses *)
-fun build_logic_map mode0 ctxt type_lits cls thss =
+fun prepare_metis_problem mode0 ctxt type_lits cls thss =
let val thy = ProofContext.theory_of ctxt
(*The modes FO and FT are sticky. HO can be downgraded to FO.*)
fun set_mode FO = FO
@@ -733,7 +733,7 @@
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
fun add_thm is_conjecture (metis_ith, isa_ith)
- {axioms, tfrees, old_skolems} : logic_map =
+ {axioms, tfrees, old_skolems} : metis_problem =
let
val (mth, tfree_lits, old_skolems) =
hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)