--- a/src/Provers/clasimp.ML Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Provers/clasimp.ML Fri Mar 13 19:58:26 2009 +0100
@@ -290,10 +290,10 @@
(* methods *)
-fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
+fun clasimp_meth tac prems ctxt = METHOD (fn facts =>
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_clasimpset_of ctxt));
-fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
+fun clasimp_meth' tac prems ctxt = METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_clasimpset_of ctxt)));
val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;