# HG changeset patch
# User blanchet
# Date 1378937266 -7200
# Node ID d4191bf88529372f884d4ffaa015a89806443e38
# Parent  eed6efba4e3f685ca4471523519ac6a76552a0af
avoid a keyword

diff -r eed6efba4e3f -r d4191bf88529 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Sep 11 23:55:47 2013 +0200
+++ b/etc/isar-keywords.el	Thu Sep 12 00:07:46 2013 +0200
@@ -319,7 +319,6 @@
     "constant"
     "constrains"
     "datatypes"
-    "defaults"
     "defines"
     "file"
     "fixes"
diff -r eed6efba4e3f -r d4191bf88529 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 23:55:47 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 12 00:07:46 2013 +0200
@@ -408,9 +408,9 @@
 discriminator associated with @{const Cons} is simply
 @{term "\<lambda>xs. \<not> null xs"}.
 
-The @{text "defaults"} keyword following the @{const Nil} constructor specifies
-a default value for selectors associated with other constructors. Here, it is
-used to ensure that the tail of the empty list is itself (instead of being left
+The @{text defaults} clause following the @{const Nil} constructor specifies a
+default value for selectors associated with other constructors. Here, it is used
+to ensure that the tail of the empty list is itself (instead of being left
 unspecified).
 
 Because @{const Nil} is a nullary constructor, it is also possible to use
diff -r eed6efba4e3f -r d4191bf88529 src/HOL/BNF/BNF_FP_Base.thy
--- a/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 11 23:55:47 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy	Thu Sep 12 00:07:46 2013 +0200
@@ -11,8 +11,6 @@
 
 theory BNF_FP_Base
 imports BNF_Comp BNF_Ctr_Sugar
-keywords
-  "defaults"
 begin
 
 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
diff -r eed6efba4e3f -r d4191bf88529 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Sep 11 23:55:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Sep 12 00:07:46 2013 +0200
@@ -1538,7 +1538,7 @@
   (Parse.typ >> pair Binding.empty);
 
 val parse_defaults =
-  @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
+  @{keyword "("} |-- Parse.reserved "defaults" |-- Scan.repeat parse_bound_term --| @{keyword ")"};
 
 val parse_type_arg_constrained =
   Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
@@ -1554,8 +1554,6 @@
 
 val no_map_rel = (Binding.empty, Binding.empty);
 
-(* "map" and "rel" are purposedly not registered as keywords, because they are short and nice names
-   that we don't want them to be highlighted everywhere. *)
 fun extract_map_rel ("map", b) = apfst (K b)
   | extract_map_rel ("rel", b) = apsnd (K b)
   | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
diff -r eed6efba4e3f -r d4191bf88529 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 11 23:55:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Sep 12 00:07:46 2013 +0200
@@ -2903,17 +2903,11 @@
   Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
     (parse_co_datatype_cmd Greatest_FP construct_gfp);
 
-local
-
 val option_parser = Parse.group (fn () => "option") (Parse.reserved "sequential" >> K true);
 
-in
-
 val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorec"}
   "define primitive corecursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) --
     (Parse.fixes -- Parse_Spec.where_alt_specs) >> uncurry add_primcorec_cmd);
- 
-end
 
 end;