# HG changeset patch
# User blanchet
# Date 1391452322 -3600
# Node ID 6f77310a0907f2002b3ca8ec935546f467b5f166
# Parent  42cf5802d36a0ae50786ead283af58d679678d6a
proper fresh name generation

diff -r 42cf5802d36a -r 6f77310a0907 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 08:23:21 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -137,9 +137,7 @@
         val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
 
         fun massage_meths (meths as meth :: _) =
-          if not try0_isar then [meth]
-          else if smt then SMT_Method :: meths
-          else meths
+          if not try0_isar then [meth] else if smt then SMT_Method :: meths else meths
 
         val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
         val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
diff -r 42cf5802d36a -r 6f77310a0907 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- 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))