--- a/src/HOL/Import/import_syntax.ML Fri Aug 27 16:29:12 2010 +0200
+++ b/src/HOL/Import/import_syntax.ML Fri Aug 27 16:32:11 2010 +0200
@@ -148,11 +148,11 @@
val _ = TextIO.closeIn is
val orig_source = Source.of_string inp
val symb_source = Symbol.source {do_recover = false} orig_source
- val lexes = Unsynchronized.ref
- (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
+ val lexes =
+ (Scan.make_lexicon
+ (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
Scan.empty_lexicon)
- val get_lexes = fn () => !lexes
- val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source
+ val token_source = Token.source {do_recover = NONE} (K lexes) Position.start symb_source
val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
val import_segmentP = Parse.$$$ "import_segment" |-- import_segment
val type_mapsP = Parse.$$$ "type_maps" |-- type_maps