1.1 --- a/src/Pure/Syntax/syntax.ML Sat Jul 07 00:14:54 2007 +0200
1.2 +++ b/src/Pure/Syntax/syntax.ML Sat Jul 07 00:14:56 2007 +0200
1.3 @@ -55,7 +55,7 @@
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 -> string * real)) list -> syntax -> syntax
1.8 + val extend_tokentrfuns: (string * string * (string -> string * int)) list -> syntax -> syntax
1.9 val remove_const_gram: (string -> bool) ->
1.10 mode -> (string * typ * mixfix) list -> syntax -> syntax
1.11 val extend_trrules: Proof.context -> (string -> bool) -> syntax ->
1.12 @@ -183,7 +183,7 @@
1.13 print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
1.14 print_ruletab: ruletab,
1.15 print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
1.16 - tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list,
1.17 + tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
1.18 prtabs: Printer.prtabs} * stamp;
1.19
1.20 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;