# HG changeset patch
# User paulson
# Date 1197995845 -3600
# Node ID 31232fe5a6add51427c9d89d3d5cf6f17d375924
# Parent  eda4958ab0d233eadda737c3c1e279139fb3d83a
Deleted redundant setmp calls

diff -r eda4958ab0d2 -r 31232fe5a6ad src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Tue Dec 18 16:26:46 2007 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Tue Dec 18 17:37:25 2007 +0100
@@ -621,10 +621,7 @@
   val metisH_tac = metis_general_tac ResAtp.Hol;
 
   fun method mode = Method.thms_ctxt_args (fn ths => fn ctxt =>
-    Method.SIMPLE_METHOD'
-      (setmp ResHolClause.typ_level ResHolClause.T_CONST  (*constant-typed*)
-        (setmp ResHolClause.minimize_applies false        (*avoid this optimization*)
-          (CHANGED_PROP o metis_general_tac mode ctxt ths))));
+    Method.SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths));
 
   val setup =
     type_lits_setup #>