# HG changeset patch
# User wenzelm
# Date 1194786009 -3600
# Node ID 8bfa6566ac6b5ff4eda2d9a2c00dca0fda6b8829
# Parent  3e58c7cb5a73bf8d1085db2bbbb1b997ab1455a2
syntax operations: turned extend'' into update'' (absorb duplicates);

diff -r 3e58c7cb5a73 -r 8bfa6566ac6b src/Pure/Isar/local_syntax.ML
--- a/src/Pure/Isar/local_syntax.ML	Sun Nov 11 14:00:08 2007 +0100
+++ b/src/Pure/Isar/local_syntax.ML	Sun Nov 11 14:00:09 2007 +0100
@@ -63,7 +63,7 @@
       | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls;
     val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
     val local_syntax = thy_syntax
-      |> Syntax.extend_trfuns
+      |> Syntax.update_trfuns
           (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
            map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
       |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
diff -r 3e58c7cb5a73 -r 8bfa6566ac6b src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Nov 11 14:00:08 2007 +0100
+++ b/src/Pure/sign.ML	Sun Nov 11 14:00:09 2007 +0100
@@ -586,7 +586,7 @@
 
 fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
-    val syn' = Syntax.extend_type_gram types syn;
+    val syn' = Syntax.update_type_gram types syn;
     val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
     val tsig' = Type.add_types naming decls tsig;
   in (naming, syn', tsig', consts) end);
@@ -603,7 +603,7 @@
 
 fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
-    val syn' = Syntax.extend_consts ns syn;
+    val syn' = Syntax.update_consts ns syn;
     val tsig' = Type.add_nonterminals naming ns tsig;
   in (naming, syn', tsig', consts) end);
 
@@ -614,7 +614,7 @@
   thy |> map_sign (fn (naming, syn, tsig, consts) =>
     let
       val ctxt = ProofContext.init thy;
-      val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn;
+      val syn' = Syntax.update_type_gram [(a, length vs, mx)] syn;
       val a' = Syntax.type_name a mx;
       val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
         handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
@@ -635,7 +635,7 @@
         cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
   in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
 
-fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
+fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
 
 val add_modesyntax = gen_add_syntax Syntax.parse_typ;
 val add_modesyntax_i = gen_add_syntax (K I);
@@ -718,7 +718,7 @@
 fun primitive_class (bclass, classes) thy =
   thy |> map_sign (fn (naming, syn, tsig, consts) =>
     let
-      val syn' = Syntax.extend_consts [bclass] syn;
+      val syn' = Syntax.update_consts [bclass] syn;
       val tsig' = Type.add_class (pp thy) naming (bclass, classes) tsig;
     in (naming, syn', tsig', consts) end)
   |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
@@ -740,10 +740,10 @@
 
 in
 
-val add_trfuns = gen_add_trfuns Syntax.extend_trfuns Syntax.non_typed_tr';
-val add_trfunsT = gen_add_trfunsT Syntax.extend_trfuns;
-val add_advanced_trfuns = gen_add_trfuns Syntax.extend_advanced_trfuns Syntax.non_typed_tr'';
-val add_advanced_trfunsT = gen_add_trfunsT Syntax.extend_advanced_trfuns;
+val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax.non_typed_tr';
+val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns;
+val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax.non_typed_tr'';
+val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns;
 
 end;
 
@@ -757,9 +757,9 @@
   let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
   in f (ProofContext.init thy) (is_logtype thy) syn rules syn end);
 
-val add_trrules = gen_trrules Syntax.extend_trrules;
+val add_trrules = gen_trrules Syntax.update_trrules;
 val del_trrules = gen_trrules Syntax.remove_trrules;
-val add_trrules_i = map_syn o Syntax.extend_trrules_i;
+val add_trrules_i = map_syn o Syntax.update_trrules_i;
 val del_trrules_i = map_syn o Syntax.remove_trrules_i;