disable new polymorphic code for now, until remaining issues in "equality_inf" are resolved

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Jun 12 11:11:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Jun 12 11:12:31 2010 +0200
@@ -398,7 +398,12 @@
     let
       val ctxt0 = Variable.global_thm_context th
       val (nnfth, ctxt) = to_nnf th ctxt0
+
+      val inline = false
+(*
+FIXME: Reintroduce code:
       val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
+*)
       val defs = skolem_theorems_of_assume inline s nnfth
       val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
     in