--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 10:36:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 10:56:45 2010 +0200
@@ -608,7 +608,7 @@
(* ------------------------------------------------------------------------- *)
fun cnf_helper_theorem thy raw th =
- if raw then th else the_single (cnf_axiom thy th)
+ if raw then th else the_single (cnf_axiom thy false th)
fun type_ext thy tms =
let val subs = tfree_classes_of_terms tms
@@ -724,7 +724,7 @@
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
val th_cls_pairs =
- map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
+ map (fn th => (Thm.get_name_hint th, cnf_axiom thy false th)) ths0
val ths = maps #2 th_cls_pairs
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls