1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 08:23:21 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
     1.3 @@ -137,9 +137,7 @@
     1.4          val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
     1.5  
     1.6          fun massage_meths (meths as meth :: _) =
     1.7 -          if not try0_isar then [meth]
     1.8 -          else if smt then SMT_Method :: meths
     1.9 -          else meths
    1.10 +          if not try0_isar then [meth] else if smt then SMT_Method :: meths else meths
    1.11  
    1.12          val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
    1.13          val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params

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