src/Tools/Code/code_printer.ML
changeset 69485 b734ff28e405
parent 68028 1f9f973eed2a
child 69593 3dda49e08b9d
--- a/src/Tools/Code/code_printer.ML	Thu Dec 20 12:40:24 2018 +0000
+++ b/src/Tools/Code/code_printer.ML	Thu Dec 20 12:55:45 2018 +0000
@@ -423,7 +423,7 @@
 type identifiers = (string list * string, string list * string, string list * string, string list * string,
   string list * string, string list * string) Code_Symbol.data;
 type printings = (const_syntax, tyco_syntax, string, unit, unit,
-    (Pretty.T * string list)) Code_Symbol.data;
+    (Pretty.T * Code_Symbol.T list)) Code_Symbol.data;
 
 datatype data = Data of { reserved: string list, identifiers: identifiers,
   printings: printings };