src/Pure/Syntax/syntax.ML
changeset 2504 f5e2288c2697
parent 2383 4127499d9b52
child 2585 8b92caca102c
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri Jan 10 10:27:57 1997 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Jan 13 09:29:55 1997 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4  
     1.5  (*the ref serves as unique id*)
     1.6  (*does not subsume typed print translations*)
     1.7 -type 'a trtab = (('a list -> 'a) * unit ref) Symtab.table;
     1.8 +type 'a trtab = (('a list -> 'a) * stamp) Symtab.table;
     1.9  
    1.10  val dest_trtab = Symtab.dest;
    1.11  
    1.12 @@ -86,7 +86,7 @@
    1.13  val empty_trtab = Symtab.null;
    1.14  
    1.15  fun extend_trtab tab trfuns name =
    1.16 -  Symtab.extend_new (tab, map (fn (c, f) => (c, (f, ref ()))) trfuns)
    1.17 +  Symtab.extend_new (tab, map (fn (c, f) => (c, (f, stamp ()))) trfuns)
    1.18      handle Symtab.DUPS cs => err_dup_trfuns name cs;
    1.19  
    1.20  fun merge_trtabs tab1 tab2 name =
    1.21 @@ -133,7 +133,7 @@
    1.22      parse_ast_trtab: ast trtab,
    1.23      parse_ruletab: ruletab,
    1.24      parse_trtab: term trtab,
    1.25 -    print_trtab: ((typ -> term list -> term) * unit ref) Symtab.table,
    1.26 +    print_trtab: ((typ -> term list -> term) * stamp) Symtab.table,
    1.27      print_ruletab: ruletab,
    1.28      print_ast_trtab: ast trtab,
    1.29      prtabs: prtabs};