# HG changeset patch
# User wenzelm
# Date 953927955 -3600
# Node ID c323613e4a47c420803e0feaea4981623cdf0ea1
# Parent  63d4f3ea2e708950e0bb2fd3cd9d904023340f74
arith method: HEADGOAL;

diff -r 63d4f3ea2e70 -r c323613e4a47 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Mar 24 17:29:51 2000 +0100
+++ b/src/HOL/Arith.ML	Fri Mar 24 20:59:15 2000 +0100
@@ -1034,7 +1034,7 @@
 (* 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