# HG changeset patch
# User wenzelm
# Date 949093035 -3600
# Node ID 9d2ac5439089509b924fae6f3dca060902acc8e8
# Parent  7574835ed01e8f5406ca7571f16ddd6377911596
HEADGOAL;

diff -r 7574835ed01e -r 9d2ac5439089 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Jan 28 21:56:55 2000 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Jan 28 21:57:15 2000 +0100
@@ -520,7 +520,7 @@
 (* method *)
 
 val record_split_method =
-  ("record_split", Method.no_args (Method.METHOD0 (FINDGOAL record_split_tac)),
+  ("record_split", Method.no_args (Method.METHOD0 (HEADGOAL record_split_tac)),
     "split record fields");
 
 
diff -r 7574835ed01e -r 9d2ac5439089 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Fri Jan 28 21:56:55 2000 +0100
+++ b/src/Provers/clasimp.ML	Fri Jan 28 21:57:15 2000 +0100
@@ -158,7 +158,7 @@
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
 
 fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
-  FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
+  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset 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';
diff -r 7574835ed01e -r 9d2ac5439089 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Jan 28 21:56:55 2000 +0100
+++ b/src/Provers/classical.ML	Fri Jan 28 21:57:15 2000 +0100
@@ -1149,7 +1149,7 @@
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
 
 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
-  FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
+  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
 
 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
diff -r 7574835ed01e -r 9d2ac5439089 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Jan 28 21:56:55 2000 +0100
+++ b/src/Provers/simplifier.ML	Fri Jan 28 21:57:15 2000 +0100
@@ -487,7 +487,7 @@
 
 fun simp_method tac =
   (fn prems => fn ctxt => Method.METHOD (fn facts =>
-    FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
+    HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
   |> Method.bang_sectioned_args simp_modifiers';