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