--- a/src/Pure/Isar/token.ML Wed Aug 08 22:14:39 2012 +0200
+++ b/src/Pure/Isar/token.ML Thu Aug 09 12:39:05 2012 +0200
@@ -53,9 +53,9 @@
val closure: T -> T
val ident_or_symbolic: string -> bool
val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
- val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+ val source': {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
(Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
- val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+ val source: {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a