diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Mon Apr 06 17:06:48 2015 +0200
@@ -219,7 +219,7 @@
   end
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "case_of_simps"}
+  Outer_Syntax.local_theory @{command_keyword case_of_simps}
     "turn a list of equations into a case expression"
     (Parse_Spec.opt_thm_name ":"  -- Parse.xthms1 >> case_of_simps_cmd)
 
@@ -227,7 +227,7 @@
   Parse.xthms1 --| @{keyword ")"}
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "simps_of_case"}
+  Outer_Syntax.local_theory @{command_keyword simps_of_case}
     "perform case split on rule"
     (Parse_Spec.opt_thm_name ":"  -- Parse.xthm --
       Scan.optional parse_splits [] >> simps_of_case_cmd)