# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID 123f0944e29fc52b5e5eb453b0fea04ff940fc21
# Parent  e88e974c4846a0d18d7f20fcd7cdaa34959a11eb
tuning

diff -r e88e974c4846 -r 123f0944e29f src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue May 31 16:38:36 2011 +0200
@@ -199,18 +199,14 @@
 val has_tvar =
   exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
 
+fun method modes ths ctxt facts =
+  let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
+    HEADGOAL (Method.insert_tac nonschem_facts THEN'
+              CHANGED_PROP o generic_metis_tac modes ctxt (schem_facts @ ths))
+  end
 fun setup_method (modes as mode :: _) =
   Method.setup (method_binding_for_mode mode)
-    (Attrib.thms >> (fn ths => fn ctxt =>
-       METHOD (fn facts =>
-                  let
-                    val (schem_facts, nonschem_facts) =
-                      List.partition has_tvar facts
-                  in
-                    HEADGOAL (Method.insert_tac nonschem_facts THEN'
-                              CHANGED_PROP
-                              o generic_metis_tac modes ctxt (schem_facts @ ths))
-                  end)))
+               (Attrib.thms >> (METHOD oo method modes))
 
 val setup =
   [(metis_modes, "Metis for FOL and HOL problems"),