# HG changeset patch
# User blanchet
# Date 1335357201 -7200
# Node ID 11b4395aaf0ce7dac07cc4f6dafbd0bcea57883c
# Parent  792634c6679e013b326bcd25f55075075e5c12e7
remove too aggressive skolemization optimization (prevented discovery of a model in SYN994^1)

diff -r 792634c6679e -r 11b4395aaf0c src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Apr 25 14:33:21 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Apr 25 14:33:21 2012 +0200
@@ -564,21 +564,17 @@
            else if is_positive_existential polar quant_s then
              let
                val j = length (!skolems) + 1
-               val (js', (ss', Ts')) =
-                 js ~~ (ss ~~ Ts)
-                 |> filter (fn (j, _) => loose_bvar1 (t, j + 1))
-                 |> ListPair.unzip ||> ListPair.unzip
              in
-               if skolemizable andalso length js' <= skolem_depth then
+               if skolemizable andalso length js <= skolem_depth then
                  let
-                   val sko_s = skolem_prefix_for (length js') j ^ abs_s
-                   val _ = Unsynchronized.change skolems (cons (sko_s, ss'))
-                   val sko_t = list_comb (Const (sko_s, rev Ts' ---> abs_T),
-                                          map Bound (rev js'))
+                   val sko_s = skolem_prefix_for (length js) j ^ abs_s
+                   val _ = Unsynchronized.change skolems (cons (sko_s, ss))
+                   val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
+                                          map Bound (rev js))
                    val abs_t = Abs (abs_s, abs_T,
                                     aux ss Ts (incrs js) skolemizable polar t)
                  in
-                   if null js' then
+                   if null js then
                      s_betapply Ts (abs_t, sko_t)
                    else
                      Const (@{const_name Let}, abs_T --> quant_T) $ sko_t