src/Tools/Code/code_printer.ML
changeset 36969 f5417836dbea
parent 36754 403585a89772
child 36970 01594f816e3a
     1.1 --- a/src/Tools/Code/code_printer.ML	Mon May 17 15:05:32 2010 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Mon May 17 15:11:25 2010 +0200
     1.3 @@ -72,9 +72,9 @@
     1.4    val parse_infix: ('a -> 'b) -> lrx * int -> string
     1.5      -> int * ((fixity -> 'b -> Pretty.T)
     1.6      -> fixity -> 'a list -> Pretty.T)
     1.7 -  val parse_syntax: ('a -> 'b) -> OuterParse.token list
     1.8 +  val parse_syntax: ('a -> 'b) -> Token.T list
     1.9      -> (int * ((fixity -> 'b -> Pretty.T)
    1.10 -    -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
    1.11 +    -> fixity -> 'a list -> Pretty.T)) option * Token.T list
    1.12    val simple_const_syntax: simple_const_syntax -> proto_const_syntax
    1.13    val activate_const_syntax: theory -> literals
    1.14      -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming