src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
changeset 59936 b8ffc3dc9e24
parent 59873 2d929c178283
child 59945 cfbaee8cdf1d
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -112,8 +112,8 @@
     1.4  fun unexpected_corec_call ctxt eqns t =
     1.5    error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
     1.6  fun use_primcorecursive () =
     1.7 -  error ("\"auto\" failed (try " ^ quote (#1 @{command_spec "primcorecursive"}) ^ " instead of " ^
     1.8 -    quote (#1 @{command_spec "primcorec"}) ^ ")");
     1.9 +  error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^
    1.10 +    quote (#1 @{command_keyword primcorec}) ^ ")");
    1.11  
    1.12  datatype corec_option =
    1.13    Plugins_Option of Proof.context -> Plugin_Name.filter |
    1.14 @@ -1551,13 +1551,13 @@
    1.15  val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
    1.16    ((Parse.prop >> pair Attrib.empty_binding) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
    1.17  
    1.18 -val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
    1.19 +val _ = Outer_Syntax.local_theory_to_proof @{command_keyword primcorecursive}
    1.20    "define primitive corecursive functions"
    1.21    ((Scan.optional (@{keyword "("} |--
    1.22        Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
    1.23      (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorecursive_cmd);
    1.24  
    1.25 -val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
    1.26 +val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
    1.27    "define primitive corecursive functions"
    1.28    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
    1.29        --| @{keyword ")"}) []) --