src/HOL/Tools/lin_arith.ML

--- a/src/HOL/Tools/lin_arith.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -914,7 +914,7 @@
 
 fun arith_method src =
   Method.syntax Args.bang_facts src
-  #> (fn (prems, ctxt) => Method.METHOD (fn facts =>
+  #> (fn (prems, ctxt) => METHOD (fn facts =>
       HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
       THEN' arith_tac ctxt)));