diff -r 5610c4acb48d -r 24914e42b857 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Sep 13 22:29:37 2000 +0200
+++ b/src/Provers/splitter.ML	Wed Sep 13 22:31:19 2000 +0200
@@ -417,8 +417,8 @@
 
 val split_modifiers =
  [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
-  Args.$$$ splitN -- Args.$$$ "add" -- Args.colon >> K (I, split_add_local),
-  Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)];
+  Args.$$$ splitN -- Args.$$$ Args.addN -- Args.colon >> K (I, split_add_local),
+  Args.$$$ splitN -- Args.$$$ Args.delN -- Args.colon >> K (I, split_del_local)];
 
 val split_args = #2 oo Method.syntax (Args.mode "asm" -- Attrib.local_thms);