syntax operations: turned extend'' into update'' (absorb duplicates);
authorwenzelm
Sun Nov 11 14:00:09 2007 +0100 (2007-11-11)
changeset 253908bfa6566ac6b
parent 25389 3e58c7cb5a73
child 25391 783e5de2a6c7
syntax operations: turned extend'' into update'' (absorb duplicates);
src/Pure/Isar/local_syntax.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/local_syntax.ML	Sun Nov 11 14:00:08 2007 +0100
     1.2 +++ b/src/Pure/Isar/local_syntax.ML	Sun Nov 11 14:00:09 2007 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4        | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls;
     1.5      val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
     1.6      val local_syntax = thy_syntax
     1.7 -      |> Syntax.extend_trfuns
     1.8 +      |> Syntax.update_trfuns
     1.9            (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
    1.10             map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
    1.11        |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
     2.1 --- a/src/Pure/sign.ML	Sun Nov 11 14:00:08 2007 +0100
     2.2 +++ b/src/Pure/sign.ML	Sun Nov 11 14:00:09 2007 +0100
     2.3 @@ -586,7 +586,7 @@
     2.4  
     2.5  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
     2.6    let
     2.7 -    val syn' = Syntax.extend_type_gram types syn;
     2.8 +    val syn' = Syntax.update_type_gram types syn;
     2.9      val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
    2.10      val tsig' = Type.add_types naming decls tsig;
    2.11    in (naming, syn', tsig', consts) end);
    2.12 @@ -603,7 +603,7 @@
    2.13  
    2.14  fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    2.15    let
    2.16 -    val syn' = Syntax.extend_consts ns syn;
    2.17 +    val syn' = Syntax.update_consts ns syn;
    2.18      val tsig' = Type.add_nonterminals naming ns tsig;
    2.19    in (naming, syn', tsig', consts) end);
    2.20  
    2.21 @@ -614,7 +614,7 @@
    2.22    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    2.23      let
    2.24        val ctxt = ProofContext.init thy;
    2.25 -      val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn;
    2.26 +      val syn' = Syntax.update_type_gram [(a, length vs, mx)] syn;
    2.27        val a' = Syntax.type_name a mx;
    2.28        val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    2.29          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
    2.30 @@ -635,7 +635,7 @@
    2.31          cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
    2.32    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
    2.33  
    2.34 -fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
    2.35 +fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
    2.36  
    2.37  val add_modesyntax = gen_add_syntax Syntax.parse_typ;
    2.38  val add_modesyntax_i = gen_add_syntax (K I);
    2.39 @@ -718,7 +718,7 @@
    2.40  fun primitive_class (bclass, classes) thy =
    2.41    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    2.42      let
    2.43 -      val syn' = Syntax.extend_consts [bclass] syn;
    2.44 +      val syn' = Syntax.update_consts [bclass] syn;
    2.45        val tsig' = Type.add_class (pp thy) naming (bclass, classes) tsig;
    2.46      in (naming, syn', tsig', consts) end)
    2.47    |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
    2.48 @@ -740,10 +740,10 @@
    2.49  
    2.50  in
    2.51  
    2.52 -val add_trfuns = gen_add_trfuns Syntax.extend_trfuns Syntax.non_typed_tr';
    2.53 -val add_trfunsT = gen_add_trfunsT Syntax.extend_trfuns;
    2.54 -val add_advanced_trfuns = gen_add_trfuns Syntax.extend_advanced_trfuns Syntax.non_typed_tr'';
    2.55 -val add_advanced_trfunsT = gen_add_trfunsT Syntax.extend_advanced_trfuns;
    2.56 +val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax.non_typed_tr';
    2.57 +val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns;
    2.58 +val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax.non_typed_tr'';
    2.59 +val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns;
    2.60  
    2.61  end;
    2.62  
    2.63 @@ -757,9 +757,9 @@
    2.64    let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
    2.65    in f (ProofContext.init thy) (is_logtype thy) syn rules syn end);
    2.66  
    2.67 -val add_trrules = gen_trrules Syntax.extend_trrules;
    2.68 +val add_trrules = gen_trrules Syntax.update_trrules;
    2.69  val del_trrules = gen_trrules Syntax.remove_trrules;
    2.70 -val add_trrules_i = map_syn o Syntax.extend_trrules_i;
    2.71 +val add_trrules_i = map_syn o Syntax.update_trrules_i;
    2.72  val del_trrules_i = map_syn o Syntax.remove_trrules_i;
    2.73  
    2.74