--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 21 18:45:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 22 01:21:52 2010 +0200
@@ -409,6 +409,7 @@
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
+ val inline = false (* FIXME: temporary *)
val defs = skolem_theorems_of_assume inline s nnfth
val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
in