# HG changeset patch
# User smolkas
# Date 1358359360 -3600
# Node ID 02ed5abcc0e509d8ed13e445d69864d8c9096623
# Parent  a86708897266a90bfc1f7f6acb6f19d04cbdb938
use Pure instead of HOL connectives

diff -r a86708897266 -r 02ed5abcc0e5 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 16 12:55:29 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 16 19:02:40 2013 +0100
@@ -137,24 +137,17 @@
                 (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
                    (see ~~/src/Pure/Isar/obtain.ML) *)
                 let
-                  (*val thesis = Term.Free ("thesis", HOLogic.boolT)
-                    |> HOLogic.mk_Trueprop
+                  val thesis = Term.Free ("thesis", HOLogic.boolT)
+                  val thesis_prop = thesis |> HOLogic.mk_Trueprop
                   val frees = map Term.Free xs
 
                   (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
-                  val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis))
+                  val inner_prop =
+                    fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
 
                   (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
-                  val prop = Logic.all thesis (Logic.mk_implies (inner_prop, thesis))*)
-
-                  val thesis = Term.Free ("thesis", HOLogic.boolT)
                   val prop =
-                    HOLogic.mk_imp (HOLogic.dest_Trueprop t, thesis)
-                    |> fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) xs
-                    |> rpair thesis
-                    |> HOLogic.mk_imp
-                    |> (fn t => HOLogic.mk_all ("thesis", HOLogic.boolT, t))
-                    |> HOLogic.mk_Trueprop
+                    Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
                 in
                   (prop, byline, true)
                 end