# 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;