diff -r 7590fd5ce3c7 -r f5e2288c2697 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Jan 10 10:27:57 1997 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Jan 13 09:29:55 1997 +0100
@@ -70,7 +70,7 @@
 
 (*the ref serves as unique id*)
 (*does not subsume typed print translations*)
-type 'a trtab = (('a list -> 'a) * unit ref) Symtab.table;
+type 'a trtab = (('a list -> 'a) * stamp) Symtab.table;
 
 val dest_trtab = Symtab.dest;
 
@@ -86,7 +86,7 @@
 val empty_trtab = Symtab.null;
 
 fun extend_trtab tab trfuns name =
-  Symtab.extend_new (tab, map (fn (c, f) => (c, (f, ref ()))) trfuns)
+  Symtab.extend_new (tab, map (fn (c, f) => (c, (f, stamp ()))) trfuns)
     handle Symtab.DUPS cs => err_dup_trfuns name cs;
 
 fun merge_trtabs tab1 tab2 name =
@@ -133,7 +133,7 @@
     parse_ast_trtab: ast trtab,
     parse_ruletab: ruletab,
     parse_trtab: term trtab,
-    print_trtab: ((typ -> term list -> term) * unit ref) Symtab.table,
+    print_trtab: ((typ -> term list -> term) * stamp) Symtab.table,
     print_ruletab: ruletab,
     print_ast_trtab: ast trtab,
     prtabs: prtabs};