# HG changeset patch
# User blanchet
# Date 1276544965 -7200
# Node ID 4656ef45fedfd1476ee012cda8908a20ea45ab98
# Parent  c02bd0bb276d2beec1bcbd53daa5d28f11c17c35
turn off new polymorphism code again -- a new issue popped up

diff -r c02bd0bb276d -r 4656ef45fedf src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Jun 14 20:48:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Jun 14 21:49:25 2010 +0200
@@ -407,6 +407,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