1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
     1.3 @@ -133,6 +133,8 @@
     1.4  
     1.5          val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
     1.6  
     1.7 +        val massage_meths = not try0_isar ? single o hd
     1.8 +
     1.9          val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
    1.10          val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
    1.11          val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
    1.12 @@ -161,9 +163,10 @@
    1.13            |> map (fn ((l, t), rule) =>
    1.14              let
    1.15                val (skos, meths) =
    1.16 -                if is_skolemize_rule rule then (skolems_of t, skolem_methods)
    1.17 -                else if is_arith_rule rule then ([], arith_methods)
    1.18 -                else ([], rewrite_methods)
    1.19 +                (if is_skolemize_rule rule then (skolems_of t, skolem_methods)
    1.20 +                 else if is_arith_rule rule then ([], arith_methods)
    1.21 +                 else ([], rewrite_methods))
    1.22 +                ||> massage_meths
    1.23              in
    1.24                Prove ([], skos, l, t, [], (([], []), meths))
    1.25              end)
    1.26 @@ -214,7 +217,7 @@
    1.27              accum
    1.28              |> (if tainted = [] then
    1.29                    cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
    1.30 -                               ((the_list predecessor, []), metislike_methods)))
    1.31 +                               ((the_list predecessor, []), massage_meths metislike_methods)))
    1.32                  else
    1.33                    I)
    1.34              |> rev
    1.35 @@ -230,10 +233,11 @@
    1.36  
    1.37                val deps = fold add_fact_of_dependencies gamma no_facts
    1.38                val meths =
    1.39 -                if skolem then skolem_methods
    1.40 -                else if is_arith_rule rule then arith_methods
    1.41 -                else if is_datatype_rule rule then datatype_methods
    1.42 -                else metislike_methods
    1.43 +                (if skolem then skolem_methods
    1.44 +                 else if is_arith_rule rule then arith_methods
    1.45 +                 else if is_datatype_rule rule then datatype_methods
    1.46 +                 else metislike_methods)
    1.47 +                |> massage_meths
    1.48                val by = (deps, meths)
    1.49              in
    1.50                if is_clause_tainted c then
    1.51 @@ -259,7 +263,7 @@
    1.52                val step =
    1.53                  Prove (maybe_show outer c [], [], l, t,
    1.54                    map isar_case (filter_out (null o snd) cases),
    1.55 -                  ((the_list predecessor, []), metislike_methods))
    1.56 +                  ((the_list predecessor, []), massage_meths metislike_methods))
    1.57              in
    1.58                isar_steps outer (SOME l) (step :: accum) infs
    1.59              end