src/Pure/sign.ML
changeset 25390 8bfa6566ac6b
parent 25383 2e766dd19e4f
child 25458 ba8f5e4fa336
     1.1 --- a/src/Pure/sign.ML	Sun Nov 11 14:00:08 2007 +0100
     1.2 +++ b/src/Pure/sign.ML	Sun Nov 11 14:00:09 2007 +0100
     1.3 @@ -586,7 +586,7 @@
     1.4  
     1.5  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
     1.6    let
     1.7 -    val syn' = Syntax.extend_type_gram types syn;
     1.8 +    val syn' = Syntax.update_type_gram types syn;
     1.9      val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
    1.10      val tsig' = Type.add_types naming decls tsig;
    1.11    in (naming, syn', tsig', consts) end);
    1.12 @@ -603,7 +603,7 @@
    1.13  
    1.14  fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.15    let
    1.16 -    val syn' = Syntax.extend_consts ns syn;
    1.17 +    val syn' = Syntax.update_consts ns syn;
    1.18      val tsig' = Type.add_nonterminals naming ns tsig;
    1.19    in (naming, syn', tsig', consts) end);
    1.20  
    1.21 @@ -614,7 +614,7 @@
    1.22    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.23      let
    1.24        val ctxt = ProofContext.init thy;
    1.25 -      val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn;
    1.26 +      val syn' = Syntax.update_type_gram [(a, length vs, mx)] syn;
    1.27        val a' = Syntax.type_name a mx;
    1.28        val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    1.29          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
    1.30 @@ -635,7 +635,7 @@
    1.31          cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
    1.32    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
    1.33  
    1.34 -fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
    1.35 +fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
    1.36  
    1.37  val add_modesyntax = gen_add_syntax Syntax.parse_typ;
    1.38  val add_modesyntax_i = gen_add_syntax (K I);
    1.39 @@ -718,7 +718,7 @@
    1.40  fun primitive_class (bclass, classes) thy =
    1.41    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.42      let
    1.43 -      val syn' = Syntax.extend_consts [bclass] syn;
    1.44 +      val syn' = Syntax.update_consts [bclass] syn;
    1.45        val tsig' = Type.add_class (pp thy) naming (bclass, classes) tsig;
    1.46      in (naming, syn', tsig', consts) end)
    1.47    |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
    1.48 @@ -740,10 +740,10 @@
    1.49  
    1.50  in
    1.51  
    1.52 -val add_trfuns = gen_add_trfuns Syntax.extend_trfuns Syntax.non_typed_tr';
    1.53 -val add_trfunsT = gen_add_trfunsT Syntax.extend_trfuns;
    1.54 -val add_advanced_trfuns = gen_add_trfuns Syntax.extend_advanced_trfuns Syntax.non_typed_tr'';
    1.55 -val add_advanced_trfunsT = gen_add_trfunsT Syntax.extend_advanced_trfuns;
    1.56 +val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax.non_typed_tr';
    1.57 +val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns;
    1.58 +val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax.non_typed_tr'';
    1.59 +val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns;
    1.60  
    1.61  end;
    1.62  
    1.63 @@ -757,9 +757,9 @@
    1.64    let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
    1.65    in f (ProofContext.init thy) (is_logtype thy) syn rules syn end);
    1.66  
    1.67 -val add_trrules = gen_trrules Syntax.extend_trrules;
    1.68 +val add_trrules = gen_trrules Syntax.update_trrules;
    1.69  val del_trrules = gen_trrules Syntax.remove_trrules;
    1.70 -val add_trrules_i = map_syn o Syntax.extend_trrules_i;
    1.71 +val add_trrules_i = map_syn o Syntax.update_trrules_i;
    1.72  val del_trrules_i = map_syn o Syntax.remove_trrules_i;
    1.73  
    1.74