--- 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"
--- 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
--- 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"
--- 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\")");
--- 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;