src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

         val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
           atp_proof, goal) = try isar_params ()
 
         val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
 
+        val massage_meths = not try0_isar ? single o hd
+
         val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
         val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
         val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
 
         val do_preplay = preplay_timeout <> Time.zeroTime

         val lems =
           map_filter (get_role (curry (op =) Lemma)) atp_proof
           |> map (fn ((l, t), rule) =>
             let
               val (skos, meths) =
-                if is_skolemize_rule rule then (skolems_of t, skolem_methods)
-                else if is_arith_rule rule then ([], arith_methods)
-                else ([], rewrite_methods)
+                (if is_skolemize_rule rule then (skolems_of t, skolem_methods)
+                 else if is_arith_rule rule then ([], arith_methods)
+                 else ([], rewrite_methods))
+                ||> massage_meths
             in
               Prove ([], skos, l, t, [], (([], []), meths))
             end)
 
         val bot = atp_proof |> List.last |> #1

 
         fun isar_steps outer predecessor accum [] =
             accum
             |> (if tainted = [] then
                   cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
-                               ((the_list predecessor, []), metislike_methods)))
+                               ((the_list predecessor, []), massage_meths metislike_methods)))
                 else
                   I)
             |> rev
           | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
             let

               fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
               fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
 
               val deps = fold add_fact_of_dependencies gamma no_facts
               val meths =
-                if skolem then skolem_methods
-                else if is_arith_rule rule then arith_methods
-                else if is_datatype_rule rule then datatype_methods
-                else metislike_methods
+                (if skolem then skolem_methods
+                 else if is_arith_rule rule then arith_methods
+                 else if is_datatype_rule rule then datatype_methods
+                 else metislike_methods)
+                |> massage_meths
               val by = (deps, meths)
             in
               if is_clause_tainted c then
                 (case gamma of
                   [g] =>

               val l = label_of_clause c
               val t = prop_of_clause c
               val step =
                 Prove (maybe_show outer c [], [], l, t,
                   map isar_case (filter_out (null o snd) cases),
-                  ((the_list predecessor, []), metislike_methods))
+                  ((the_list predecessor, []), massage_meths metislike_methods))
             in
               isar_steps outer (SOME l) (step :: accum) infs
             end
         and isar_proof outer fix assms lems infs =
           Proof (fix, assms, lems @ isar_steps outer NONE [] infs)