src/Pure/Syntax/syntax.ML
changeset 26704 51ee753cc2e3
parent 26684 0701201def95
child 26951 030e4a818b39
     1.1 --- a/src/Pure/Syntax/syntax.ML	Thu Apr 17 16:30:48 2008 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Apr 17 16:30:50 2008 +0200
     1.3 @@ -45,7 +45,8 @@
     1.4      (string * ((Proof.context -> term list -> term) * stamp)) list *
     1.5      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     1.6      (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
     1.7 -  val extend_tokentrfuns: (string * string * (string -> output * int)) list -> syntax -> syntax
     1.8 +  val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
     1.9 +    syntax -> syntax
    1.10    val update_const_gram: (string -> bool) ->
    1.11      mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.12    val remove_const_gram: (string -> bool) ->
    1.13 @@ -239,7 +240,7 @@
    1.14      print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
    1.15      print_ruletab: ruletab,
    1.16      print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
    1.17 -    tokentrtab: (string * (string * ((string -> output * int) * stamp)) list) list,
    1.18 +    tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
    1.19      prtabs: Printer.prtabs} * stamp;
    1.20  
    1.21  fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;