# HG changeset patch
# User blanchet
# Date 1277162512 -7200
# Node ID a5aa61b7fa740aca8fea0d49bc421ef116c2e6b7
# Parent  3da1e49459ee7280edd52be80b271ce374b41bd6
reredisable new polymorphic code

diff -r 3da1e49459ee -r a5aa61b7fa74 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- 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