--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 08:23:21 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 19:32:02 2014 +0100
@@ -110,10 +110,10 @@
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
(cf. "~~/src/Pure/Isar/obtain.ML") *)
let
- (* FIXME: generate fresh name *)
- val thesis = Free ("thesis_preplay", HOLogic.boolT)
+ val frees = map Free xs
+ val thesis =
+ Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT))
val thesis_prop = HOLogic.mk_Trueprop thesis
- val frees = map Free xs
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))