# HG changeset patch
# User blanchet
# Date 1391418858 -3600
# Node ID e887c074361414684bf48fb0de8870875ae99c2e
# Parent  236114c5eb44ba1827330a6621f31572bbe3c9c0
implemented new 'try0_isar' semantics

diff -r 236114c5eb44 -r e887c0743614 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -133,6 +133,8 @@
 
         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
@@ -161,9 +163,10 @@
           |> 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)
@@ -214,7 +217,7 @@
             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
@@ -230,10 +233,11 @@
 
               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
@@ -259,7 +263,7 @@
               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