src/Pure/Thy/present.ML
changeset 7752 7ee322caf59c
parent 7727 b52c7d773121
child 7757 b2538dccc21e
--- a/src/Pure/Thy/present.ML	Wed Oct 06 00:34:48 1999 +0200
+++ b/src/Pure/Thy/present.ML	Wed Oct 06 00:35:05 1999 +0200
@@ -17,7 +17,7 @@
   val finish: unit -> unit
   val init_theory: string -> unit
   val verbatim_source: string -> (unit -> string list) -> unit
-  val token_source: string -> (unit -> OuterLex.token list) -> unit
+  val token_source: string -> (unit -> (OuterLex.token * string option) list) -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
   val result: string -> string -> thm -> unit
   val results: string -> string -> thm list -> unit