# HG changeset patch
# User blanchet
# Date 1288084200 -7200
# Node ID a2f01956220e8fb1dd4345fd974548329ca3b5da
# Parent  d170c322157ad96d524e51ac020005c3f8abd77f
renaming

diff -r d170c322157a -r a2f01956220e src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 26 11:10:00 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 d170c322157a -r a2f01956220e src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 26 11:00:17 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 26 11:10:00 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)