src/HOL/Tools/Function/fun.ML
changeset 46961 5c6955f487e5
parent 45639 efddd75c741e
child 48099 e7e647949c95
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -170,9 +170,9 @@
     1.4  
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.local_theory' "fun" "define general recursive functions (short version)"
     1.8 -  Keyword.thy_decl
     1.9 -  (function_parser fun_config
    1.10 -     >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
    1.11 +  Outer_Syntax.local_theory' @{command_spec "fun"}
    1.12 +    "define general recursive functions (short version)"
    1.13 +    (function_parser fun_config
    1.14 +      >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
    1.15  
    1.16  end