avoid a keyword
authorblanchet
Thu Sep 12 00:07:46 2013 +0200 (2013-09-12)
changeset 53553d4191bf88529
parent 53552 eed6efba4e3f
child 53554 78fe0002024d
avoid a keyword
etc/isar-keywords.el
src/Doc/Datatypes/Datatypes.thy
src/HOL/BNF/BNF_FP_Base.thy
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_gfp.ML
     1.1 --- a/etc/isar-keywords.el	Wed Sep 11 23:55:47 2013 +0200
     1.2 +++ b/etc/isar-keywords.el	Thu Sep 12 00:07:46 2013 +0200
     1.3 @@ -319,7 +319,6 @@
     1.4      "constant"
     1.5      "constrains"
     1.6      "datatypes"
     1.7 -    "defaults"
     1.8      "defines"
     1.9      "file"
    1.10      "fixes"
     2.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 23:55:47 2013 +0200
     2.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 12 00:07:46 2013 +0200
     2.3 @@ -408,9 +408,9 @@
     2.4  discriminator associated with @{const Cons} is simply
     2.5  @{term "\<lambda>xs. \<not> null xs"}.
     2.6  
     2.7 -The @{text "defaults"} keyword following the @{const Nil} constructor specifies
     2.8 -a default value for selectors associated with other constructors. Here, it is
     2.9 -used to ensure that the tail of the empty list is itself (instead of being left
    2.10 +The @{text defaults} clause following the @{const Nil} constructor specifies a
    2.11 +default value for selectors associated with other constructors. Here, it is used
    2.12 +to ensure that the tail of the empty list is itself (instead of being left
    2.13  unspecified).
    2.14  
    2.15  Because @{const Nil} is a nullary constructor, it is also possible to use
     3.1 --- a/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 11 23:55:47 2013 +0200
     3.2 +++ b/src/HOL/BNF/BNF_FP_Base.thy	Thu Sep 12 00:07:46 2013 +0200
     3.3 @@ -11,8 +11,6 @@
     3.4  
     3.5  theory BNF_FP_Base
     3.6  imports BNF_Comp BNF_Ctr_Sugar
     3.7 -keywords
     3.8 -  "defaults"
     3.9  begin
    3.10  
    3.11  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
     4.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Sep 11 23:55:47 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Sep 12 00:07:46 2013 +0200
     4.3 @@ -1538,7 +1538,7 @@
     4.4    (Parse.typ >> pair Binding.empty);
     4.5  
     4.6  val parse_defaults =
     4.7 -  @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
     4.8 +  @{keyword "("} |-- Parse.reserved "defaults" |-- Scan.repeat parse_bound_term --| @{keyword ")"};
     4.9  
    4.10  val parse_type_arg_constrained =
    4.11    Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
    4.12 @@ -1554,8 +1554,6 @@
    4.13  
    4.14  val no_map_rel = (Binding.empty, Binding.empty);
    4.15  
    4.16 -(* "map" and "rel" are purposedly not registered as keywords, because they are short and nice names
    4.17 -   that we don't want them to be highlighted everywhere. *)
    4.18  fun extract_map_rel ("map", b) = apfst (K b)
    4.19    | extract_map_rel ("rel", b) = apsnd (K b)
    4.20    | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
     5.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 11 23:55:47 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Sep 12 00:07:46 2013 +0200
     5.3 @@ -2903,17 +2903,11 @@
     5.4    Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
     5.5      (parse_co_datatype_cmd Greatest_FP construct_gfp);
     5.6  
     5.7 -local
     5.8 -
     5.9  val option_parser = Parse.group (fn () => "option") (Parse.reserved "sequential" >> K true);
    5.10  
    5.11 -in
    5.12 -
    5.13  val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorec"}
    5.14    "define primitive corecursive functions"
    5.15    ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) --
    5.16      (Parse.fixes -- Parse_Spec.where_alt_specs) >> uncurry add_primcorec_cmd);
    5.17 - 
    5.18 -end
    5.19  
    5.20  end;