# HG changeset patch
# User blanchet
# Date 1284799432 -7200
# Node ID b96941dddd047bf563532558e8d819a2dd7ee6d9
# Parent  5df45da44bfba370a769811d96e5cd7649d1b819
preprocess "All" before doing clausification in Metis;
helps the definitional clausifier produce fewer clauses

diff -r 5df45da44bfb -r b96941dddd04 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Sep 17 17:02:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat Sep 18 10:43:52 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