# HG changeset patch
# User blanchet
# Date 1277205437 -7200
# Node ID 9ae78e12e126cb97fc1a5302cc9f4ac4667b81db
# Parent  650fae5eea93417d3167b4bad429999d9535917a
reintroduce new Sledgehammer polymorphic handling code;
this time I tested the proper version of Isabelle

diff -r 650fae5eea93 -r 9ae78e12e126 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 12:19:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 13:17:17 2010 +0200
@@ -20,6 +20,7 @@
   val type_has_topsort: typ -> bool
   val cnf_rules_pairs:
     theory -> (string * thm) list -> (thm * (string * int)) list
+  val saturate_skolem_cache: theory -> theory option
   val use_skolem_cache: bool Unsynchronized.ref
     (* for emergency use where the Skolem cache causes problems *)
   val strip_subgoal : thm -> int -> (string * typ) list * term list * term
@@ -137,7 +138,7 @@
 
 fun mk_skolem_id t =
   let val T = fastype_of t in
-    Const (@{const_name skolem_id}, T --> T) $ Envir.beta_norm t
+    Const (@{const_name skolem_id}, T --> T) $ t
   end
 
 (*Traverse a theorem, accumulating Skolem function definitions.*)
@@ -409,7 +410,6 @@
       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
diff -r 650fae5eea93 -r 9ae78e12e126 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 12:19:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 13:17:17 2010 +0200
@@ -168,6 +168,7 @@
       fun aux skolem_somes
               (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
           let
+            val t = Envir.beta_eta_contract t
             val (skolem_somes, s) =
               if i = ~1 then
                 (skolem_somes, @{const_name undefined})