added add_trrules_i;
authorwenzelm
Mon Jun 26 14:33:11 1995 +0200 (1995-06-26)
changeset 1159998a5c3451bf
parent 1158 96804ce95516
child 1160 8845eb5f0e5e
added add_trrules_i;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Mon Jun 26 14:32:26 1995 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Jun 26 14:33:11 1995 +0200
     1.3 @@ -57,7 +57,8 @@
     1.4        (string * (term list -> term)) list *
     1.5        (string * (term list -> term)) list *
     1.6        (string * (ast list -> ast)) list -> sg -> sg
     1.7 -    val add_trrules: xrule list -> sg -> sg
     1.8 +    val add_trrules: (string * string) trrule list -> sg -> sg
     1.9 +    val add_trrules_i: ast trrule list -> sg -> sg
    1.10      val add_name: string -> sg -> sg
    1.11      val make_draft: sg -> sg
    1.12      val merge: sg * sg -> sg
    1.13 @@ -434,13 +435,10 @@
    1.14    (syn, ext_tsig_subclass tsig pairs, ctab);
    1.15  
    1.16  
    1.17 -(* add syntactic translations *)
    1.18 +(* add to syntax *)
    1.19  
    1.20 -fun ext_trfuns (syn, tsig, ctab) trfuns =
    1.21 -  (Syntax.extend_trfuns syn trfuns, tsig, ctab);
    1.22 -
    1.23 -fun ext_trrules (syn, tsig, ctab) xrules =
    1.24 -  (Syntax.extend_trrules syn xrules, tsig, ctab);
    1.25 +fun ext_syn extfun (syn, tsig, ctab) args =
    1.26 +  (extfun syn args, tsig, ctab);
    1.27  
    1.28  
    1.29  (* build signature *)
    1.30 @@ -475,8 +473,9 @@
    1.31  val add_consts_i  = extend_sign ext_consts_i "#";
    1.32  val add_syntax    = extend_sign ext_syntax "#";
    1.33  val add_syntax_i  = extend_sign ext_syntax_i "#";
    1.34 -val add_trfuns    = extend_sign ext_trfuns "#";
    1.35 -val add_trrules   = extend_sign ext_trrules "#";
    1.36 +val add_trfuns    = extend_sign (ext_syn Syntax.extend_trfuns) "#";
    1.37 +val add_trrules   = extend_sign (ext_syn Syntax.extend_trrules) "#";
    1.38 +val add_trrules_i = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
    1.39  
    1.40  fun add_name name sg = extend_sign K name () sg;
    1.41  val make_draft = add_name "#";