# HG changeset patch
# User blanchet
# Date 1284971369 -7200
# Node ID 346f6d79cba664cf02514b9ca93b506d1f05101e
# Parent  49c319fff40cd078833affb745236abfa46ac44e# Parent  b96941dddd047bf563532558e8d819a2dd7ee6d9
merged

diff -r 49c319fff40c -r 346f6d79cba6 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 20 09:19:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -139,6 +139,8 @@
 val type_has_top_sort =
   exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
 
+val preproc_ss = HOL_basic_ss addsimps @{thms all_simps [symmetric]}
+
 fun generic_metis_tac mode ctxt ths i st0 =
   let
     val _ = trace_msg (fn () =>
@@ -147,9 +149,14 @@
     if exists_type type_has_top_sort (prop_of st0) then
       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
     else
-      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
-                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
-                  ctxt i st0
+      Tactical.SOLVED'
+          ((TRY o Simplifier.simp_tac preproc_ss)
+           THEN'
+           (REPEAT_DETERM o match_tac @{thms allI})
+           THEN'
+           TRY o Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
+                     (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
+                     ctxt) i st0
   end
 
 val metis_tac = generic_metis_tac HO
diff -r 49c319fff40c -r 346f6d79cba6 src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Mon Sep 20 09:19:22 2010 +0200
+++ b/src/HOL/Tools/try.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -58,18 +58,19 @@
     Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
   end
 
-fun do_named_method_on_first_goal name timeout_opt st =
+fun do_named_method (name, all_goals) timeout_opt st =
   do_generic timeout_opt
-             (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
-                      else "")) I (#goal o Proof.goal)
+             (name ^ (if all_goals andalso
+                         nprems_of (#goal (Proof.goal st)) > 1 then
+                        "[1]"
+                      else
+                        "")) I (#goal o Proof.goal)
              (apply_named_method_on_first_goal name (Proof.context_of st)) st
 
-val all_goals_named_methods = ["auto"]
-val first_goal_named_methods =
-  ["simp", "fast", "fastsimp", "force", "best", "blast", "arith"]
-val do_methods =
-  map do_named_method_on_first_goal all_goals_named_methods @
-  map do_named_method first_goal_named_methods
+val named_methods =
+  [("simp", false), ("auto", true), ("fast", false), ("fastsimp", false),
+   ("force", false), ("blast", false), ("arith", false)]
+val do_methods = map do_named_method named_methods
 
 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"