Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
authorblanchet
Mon, 20 Sep 2010 20:00:06 +0200
changeset 39594 624d6c0e220d
parent 39571 3a3d9de2ad6e
child 39596 61018b8d3e49
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
src/HOL/Tools/Sledgehammer/metis_tactics.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle