src/Tools/Code/code_printer.ML
changeset 36959 f5417836dbea
parent 36745 403585a89772
child 36960 01594f816e3a
--- a/src/Tools/Code/code_printer.ML	Mon May 17 15:05:32 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Mon May 17 15:11:25 2010 +0200
@@ -72,9 +72,9 @@
   val parse_infix: ('a -> 'b) -> lrx * int -> string
     -> int * ((fixity -> 'b -> Pretty.T)
     -> fixity -> 'a list -> Pretty.T)
-  val parse_syntax: ('a -> 'b) -> OuterParse.token list
+  val parse_syntax: ('a -> 'b) -> Token.T list
     -> (int * ((fixity -> 'b -> Pretty.T)
-    -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
+    -> fixity -> 'a list -> Pretty.T)) option * Token.T list
   val simple_const_syntax: simple_const_syntax -> proto_const_syntax
   val activate_const_syntax: theory -> literals
     -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming