diff -r f5417836dbea -r 01594f816e3a src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Mon May 17 23:54:15 2010 +0200
@@ -64,15 +64,11 @@
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
-
 val _ =
-  OuterSyntax.command "inductive_cases"
-    "create simplified instances of elimination rules (improper)" K.thy_script
-    (P.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 P.prop)
+  Outer_Syntax.command "inductive_cases"
+    "create simplified instances of elimination rules (improper)" Keyword.thy_script
+    (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
       >> (Toplevel.theory o inductive_cases));
 
 end;
 
-end;
-