diff -r 61c7875a58b8 -r d6e5fa2ba8b8 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Feb 10 02:22:13 2006 +0100
+++ b/src/Provers/splitter.ML	Fri Feb 10 02:22:16 2006 +0100
@@ -448,7 +448,7 @@
   Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
 
 fun split_meth src =
-  Method.syntax Attrib.local_thms src
+  Method.syntax Attrib.thms src
   #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths));