diff -r 9bdbcb71dc56 -r dab09e1ad594 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -520,7 +520,7 @@
 (* method *)
 
 val record_split_method =
-  ("record_split", Method.no_args (Method.METHOD0 (FIRSTGOAL record_split_tac)),
+  ("record_split", Method.no_args (Method.METHOD0 (FINDGOAL record_split_tac)),
     "split record fields");