src/Provers/clasimp.ML

   Classical.cla_modifiers @ iff_modifiers;
 
 
 (* 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;
 val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';