diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -76,15 +76,11 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val ind_cases =
-  P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
-  >> (Toplevel.theory o inductive_cases);
-
-val inductive_casesP =
+val _ =
   OuterSyntax.command "inductive_cases"
-    "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
-
-val _ = OuterSyntax.add_parsers [inductive_casesP];
+    "create simplified instances of elimination rules (improper)" K.thy_script
+    (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
+      >> (Toplevel.theory o inductive_cases));
 
 end;