# HG changeset patch
# User blanchet
# Date 1288084868 -7200
# Node ID bfc716a96e47284b51cda813a12450b797a608f7
# Parent  a88d6073b190197f4737f8a0d7cb8f51e2756a23# Parent  1348d4982a1776802a91cbbda670941e6f804390
merge

diff -r 1348d4982a17 -r bfc716a96e47 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Oct 26 11:21:08 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
diff -r 1348d4982a17 -r bfc716a96e47 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 26 11:21:08 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', _)) =>
diff -r 1348d4982a17 -r bfc716a96e47 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 26 11:20:14 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 26 11:21:08 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)