# HG changeset patch
# User wenzelm
# Date 804169991 -7200
# Node ID 998a5c3451bf81e50b5d591e0405476fb0bc1218
# Parent  96804ce955163e080be2eeecd5407f5e88905743
added add_trrules_i;

diff -r 96804ce95516 -r 998a5c3451bf src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Jun 26 14:32:26 1995 +0200
+++ b/src/Pure/sign.ML	Mon Jun 26 14:33:11 1995 +0200
@@ -57,7 +57,8 @@
       (string * (term list -> term)) list *
       (string * (term list -> term)) list *
       (string * (ast list -> ast)) list -> sg -> sg
-    val add_trrules: xrule list -> sg -> sg
+    val add_trrules: (string * string) trrule list -> sg -> sg
+    val add_trrules_i: ast trrule list -> sg -> sg
     val add_name: string -> sg -> sg
     val make_draft: sg -> sg
     val merge: sg * sg -> sg
@@ -434,13 +435,10 @@
   (syn, ext_tsig_subclass tsig pairs, ctab);
 
 
-(* add syntactic translations *)
+(* add to syntax *)
 
-fun ext_trfuns (syn, tsig, ctab) trfuns =
-  (Syntax.extend_trfuns syn trfuns, tsig, ctab);
-
-fun ext_trrules (syn, tsig, ctab) xrules =
-  (Syntax.extend_trrules syn xrules, tsig, ctab);
+fun ext_syn extfun (syn, tsig, ctab) args =
+  (extfun syn args, tsig, ctab);
 
 
 (* build signature *)
@@ -475,8 +473,9 @@
 val add_consts_i  = extend_sign ext_consts_i "#";
 val add_syntax    = extend_sign ext_syntax "#";
 val add_syntax_i  = extend_sign ext_syntax_i "#";
-val add_trfuns    = extend_sign ext_trfuns "#";
-val add_trrules   = extend_sign ext_trrules "#";
+val add_trfuns    = extend_sign (ext_syn Syntax.extend_trfuns) "#";
+val add_trrules   = extend_sign (ext_syn Syntax.extend_trrules) "#";
+val add_trrules_i = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
 
 fun add_name name sg = extend_sign K name () sg;
 val make_draft = add_name "#";