1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Jun 14 20:48:36 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Jun 14 21:49:25 2010 +0200
     1.3 @@ -407,6 +407,7 @@
     1.4        val ctxt0 = Variable.global_thm_context th
     1.5        val (nnfth, ctxt) = to_nnf th ctxt0
     1.6        val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
     1.7 +      val inline = false (* FIXME: temporary *)
     1.8        val defs = skolem_theorems_of_assume inline s nnfth
     1.9        val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
    1.10      in