1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 16 12:55:29 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 16 19:02:40 2013 +0100
     1.3 @@ -137,24 +137,17 @@
     1.4                  (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
     1.5                     (see ~~/src/Pure/Isar/obtain.ML) *)
     1.6                  let
     1.7 -                  (*val thesis = Term.Free ("thesis", HOLogic.boolT)
     1.8 -                    |> HOLogic.mk_Trueprop
     1.9 +                  val thesis = Term.Free ("thesis", HOLogic.boolT)
    1.10 +                  val thesis_prop = thesis |> HOLogic.mk_Trueprop
    1.11                    val frees = map Term.Free xs
    1.12  
    1.13                    (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
    1.14 -                  val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis))
    1.15 +                  val inner_prop =
    1.16 +                    fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
    1.17  
    1.18                    (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
    1.19 -                  val prop = Logic.all thesis (Logic.mk_implies (inner_prop, thesis))*)
    1.20 -
    1.21 -                  val thesis = Term.Free ("thesis", HOLogic.boolT)
    1.22                    val prop =
    1.23 -                    HOLogic.mk_imp (HOLogic.dest_Trueprop t, thesis)
    1.24 -                    |> fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) xs
    1.25 -                    |> rpair thesis
    1.26 -                    |> HOLogic.mk_imp
    1.27 -                    |> (fn t => HOLogic.mk_all ("thesis", HOLogic.boolT, t))
    1.28 -                    |> HOLogic.mk_Trueprop
    1.29 +                    Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
    1.30                  in
    1.31                    (prop, byline, true)
    1.32                  end