src/HOL/Tools/Function/fun_cases.ML
changeset 59936 b8ffc3dc9e24
parent 59621 291934bac95e
child 63064 2f18172214c8
     1.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop;
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.local_theory @{command_spec "fun_cases"}
     1.8 +  Outer_Syntax.local_theory @{command_keyword fun_cases}
     1.9      "create simplified instances of elimination rules for function equations"
    1.10      (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
    1.11