# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID 0af2d5dfb0ace63b6c8f448cd321810093244b73
# Parent  1977a884fef72d8b834c6ef05b0d7c9c4ff1839c
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)

diff -r 1977a884fef7 -r 0af2d5dfb0ac src/HOL/Tools/SMT2/smtlib2_isar.ML
--- a/src/HOL/Tools/SMT2/smtlib2_isar.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -40,13 +40,6 @@
 fun strip_alls (Const (@{const_name All}, _) $ Abs (s, T, body)) = strip_alls body |>> cons (s, T)
   | strip_alls t = ([], t)
 
-fun push_skolem_all_under_iff t =
-  (case strip_alls t of
-    (qs as _ :: _,
-     (t0 as Const (@{const_name HOL.eq}, _)) $ (t1 as Const (@{const_name Ex}, _) $ _) $ t2) =>
-    t0 $ HOLogic.list_all (qs, t1) $ HOLogic.list_all (qs, t2)
-  | _ => t)
-
 fun unlift_term ll_defs =
   let
     val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs
@@ -71,7 +64,6 @@
   |> simplify_bool
   |> not (null ll_defs) ? unlift_term ll_defs
   |> unskolemize_names
-  |> push_skolem_all_under_iff
   |> HOLogic.mk_Trueprop
   |> unskolemize_names