# HG changeset patch # User blanchet # Date 1392640302 -3600 # Node ID 51998cb9d6b8e8bff3c3edda62a2d4dee0b300d6 # Parent c367f4f3e5d4a87601a2dc9c3d7bd0e79c8565f1 tuning: moved code where it belongs diff -r c367f4f3e5d4 -r 51998cb9d6b8 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Feb 17 13:31:42 2014 +0100 @@ -2740,23 +2740,4 @@ Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes" (parse_co_datatype_cmd Greatest_FP construct_gfp); -val option_parser = Parse.group (fn () => "option") - ((Parse.reserved "sequential" >> K Sequential_Option) - || (Parse.reserved "exhaustive" >> K Exhaustive_Option)) - -val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|" - (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const))); - -val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"} - "define primitive corecursive functions" - ((Scan.optional (@{keyword "("} |-- - Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) -- - (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd); - -val _ = Outer_Syntax.local_theory @{command_spec "primcorec"} - "define primitive corecursive functions" - ((Scan.optional (@{keyword "("} |-- - Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) -- - (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd); - end; diff -r c367f4f3e5d4 -r 51998cb9d6b8 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Feb 17 13:31:42 2014 +0100 @@ -1373,4 +1373,23 @@ | _ => error "\"auto\" failed -- use \"primcorecursive\" instead of \"primcorec\"") goalss)) ooo add_primcorec_ursive_cmd true; +val primcorec_option_parser = Parse.group (fn () => "option") + (Parse.reserved "sequential" >> K Sequential_Option + || Parse.reserved "exhaustive" >> K Exhaustive_Option) + +val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|" + (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const))); + +val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"} + "define primitive corecursive functions" + ((Scan.optional (@{keyword "("} |-- + Parse.!!! (Parse.list1 primcorec_option_parser) --| @{keyword ")"}) []) -- + (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd); + +val _ = Outer_Syntax.local_theory @{command_spec "primcorec"} + "define primitive corecursive functions" + ((Scan.optional (@{keyword "("} |-- + Parse.!!! (Parse.list1 primcorec_option_parser) --| @{keyword ")"}) []) -- + (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd); + end; diff -r c367f4f3e5d4 -r 51998cb9d6b8 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Feb 17 13:31:42 2014 +0100 @@ -1831,8 +1831,4 @@ Outer_Syntax.local_theory @{command_spec "datatype_new"} "define new-style inductive datatypes" (parse_co_datatype_cmd Least_FP construct_lfp); -val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"} - "define primitive recursive functions" - (Parse.fixes -- Parse_Spec.where_alt_specs >> (snd oo uncurry add_primrec_cmd)); - end; diff -r c367f4f3e5d4 -r 51998cb9d6b8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Feb 17 13:31:42 2014 +0100 @@ -612,4 +612,8 @@ val simpss' = burrow (Proof_Context.export lthy' lthy) simpss; in ((ts, simpss'), Local_Theory.exit_global lthy') end; +val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"} + "define primitive recursive functions" + (Parse.fixes -- Parse_Spec.where_alt_specs >> (snd oo uncurry add_primrec_cmd)); + end;