# HG changeset patch
# User blanchet
# Date 1285005606 -7200
# Node ID 624d6c0e220dfa280f2943cac413ddcfd83d4319
# Parent  3a3d9de2ad6ee51f4f52cfcafbcb0405bc264cf0
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms

diff -r 3a3d9de2ad6e -r 624d6c0e220d src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 20 19:00:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 20 20:00:06 2010 +0200
@@ -149,13 +149,9 @@
     if exists_type type_has_top_sort (prop_of st0) then
       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
     else
-      Tactical.SOLVED'
-          ((TRY o Simplifier.full_simp_tac preproc_ss)
-           THEN' (REPEAT_DETERM o match_tac @{thms allI})
-           THEN' (REPEAT_DETERM o ematch_tac @{thms exE})
-           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
+      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