# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID f6331d78512832d2c638489ce25f107264a0b8b6
# Parent  c2ec08b0d2171c955d846fba4faf00081488dceb
removed obscure option

diff -r c2ec08b0d217 -r f6331d785128 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue May 31 16:38:36 2011 +0200
@@ -15,7 +15,6 @@
   val metisX_N : string
   val trace : bool Config.T
   val verbose : bool Config.T
-  val type_lits : bool Config.T
   val new_skolemizer : bool Config.T
   val metis_tac : Proof.context -> thm list -> int -> tactic
   val metisF_tac : Proof.context -> thm list -> int -> tactic
@@ -42,7 +41,6 @@
 val metisFT_N = Binding.qualified_name_of (method_binding_for_mode FT)
 val metisX_N = Binding.qualified_name_of (method_binding_for_mode New)
 
-val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true)
 val new_skolemizer =
   Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
 
@@ -73,7 +71,6 @@
 (* Main function to start Metis proof and reconstruction *)
 fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 =
   let val thy = Proof_Context.theory_of ctxt
-      val type_lits = Config.get ctxt type_lits
       val new_skolemizer =
         Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
       val th_cls_pairs =
@@ -88,7 +85,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}) =
-        prepare_metis_problem mode ctxt type_lits cls thss
+        prepare_metis_problem mode ctxt cls thss
       val _ = if null tfrees then ()
               else (trace_msg ctxt (fn () => "TFREE CLAUSES");
                     app (fn TyLitFree ((s, _), (s', _)) =>
diff -r c2ec08b0d217 -r f6331d785128 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -25,8 +25,7 @@
   val reveal_old_skolem_terms : (string * term) list -> term -> term
   val string_of_mode : mode -> string
   val prepare_metis_problem :
-    mode -> Proof.context -> bool -> thm list -> thm list list
-    -> mode * metis_problem
+    mode -> Proof.context -> thm list -> thm list list -> mode * metis_problem
 end
 
 structure Metis_Translate : METIS_TRANSLATE =
@@ -207,7 +206,7 @@
 fun metis_of_tfree tf =
   Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
 
-fun hol_thm_to_fol is_conjecture ctxt type_lits mode j old_skolems th =
+fun hol_thm_to_fol is_conjecture ctxt mode j old_skolems th =
   let
     val thy = Proof_Context.theory_of ctxt
     val (old_skolems, (mlits, types_sorts)) =
@@ -222,8 +221,7 @@
       let
         val tylits = types_sorts |> filter_out (has_default_sort ctxt)
                                  |> raw_type_literals_for_types
-        val mtylits =
-          if type_lits then map (metis_of_type_literals false) tylits else []
+        val mtylits = map (metis_of_type_literals false) tylits
       in
         (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
          old_skolems)
@@ -295,9 +293,9 @@
   end;
 
 (* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem New ctxt type_lits cls thss =
+fun prepare_metis_problem New ctxt cls thss =
     error "Not implemented yet"
-  | prepare_metis_problem mode ctxt type_lits cls thss =
+  | prepare_metis_problem mode ctxt cls thss =
     let
       val thy = Proof_Context.theory_of ctxt
       (* The modes FO and FT are sticky. HO can be downgraded to FO. *)
@@ -312,8 +310,8 @@
                   {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)
-                           old_skolems metis_ith
+            hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems
+                           metis_ith
         in
            {axioms = (mth, isa_ith) :: axioms,
             tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}