src/HOL/Tools/metis_tools.ML
changeset 24958 ff15f76741bd
parent 24940 8f9dea697b8d
child 24974 a2f15968a6f2
--- a/src/HOL/Tools/metis_tools.ML	Thu Oct 11 15:57:29 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 11 15:59:31 2007 +0200
@@ -529,9 +529,11 @@
         tfrees = tfrees};
         
   (* Function to generate metis clauses, including comb and type clauses *)
-  fun build_map mode thy ctxt cls ths =
-    let val isFO = (mode = ResAtp.Fol) orelse
-                    (mode <> ResAtp.Hol andalso ResAtp.is_fol_thms (cls @ ths))
+  fun build_map mode ctxt cls ths =
+    let val thy = ProofContext.theory_of ctxt
+        val all_thms_FO = forall (Meson.is_fol_term thy o prop_of)
+        val isFO = (mode = ResAtp.Fol) orelse
+                   (mode <> ResAtp.Hol andalso all_thms_FO (cls @ ths))
         val lmap0 = foldl (add_thm true ctxt) 
                           {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls
         val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths
@@ -559,8 +561,7 @@
 
   (* Main function to start metis prove and reconstruction *)
   fun FOL_SOLVE mode ctxt cls ths0 =
-    let val thy = ProofContext.theory_of ctxt
-        val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0
+    let val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0
         val ths = List.concat (map #2 th_cls_pairs)
         val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
                 else ();
@@ -568,7 +569,7 @@
         val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls
         val _ = Output.debug (fn () => "THEOREM CLAUSES")
         val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths
-        val {isFO,axioms,tfrees} = build_map mode thy ctxt cls ths
+        val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
         val _ = if null tfrees then ()
                 else (Output.debug (fn () => "TFREE CLAUSES");
                       app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)