src/HOL/Arith.ML

 
 
 (* proof method setup *)
 
 fun arith_method prems =
-  Method.METHOD (fn facts => FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
+  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
 
 val arith_setup =
  [Method.add_methods
   [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts , "decide linear arithmethic")]];