src/HOL/Import/import_syntax.ML
changeset 38803 38b68972721b
parent 37165 c2e27ae53c2a
child 40526 ca3c6b1bfcdb
     1.1 --- a/src/HOL/Import/import_syntax.ML	Fri Aug 27 16:29:12 2010 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Fri Aug 27 16:32:11 2010 +0200
     1.3 @@ -148,11 +148,11 @@
     1.4          val _ = TextIO.closeIn is
     1.5          val orig_source = Source.of_string inp
     1.6          val symb_source = Symbol.source {do_recover = false} orig_source
     1.7 -        val lexes = Unsynchronized.ref
     1.8 -          (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
     1.9 +        val lexes =
    1.10 +          (Scan.make_lexicon
    1.11 +            (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
    1.12                    Scan.empty_lexicon)
    1.13 -        val get_lexes = fn () => !lexes
    1.14 -        val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source
    1.15 +        val token_source = Token.source {do_recover = NONE} (K lexes) Position.start symb_source
    1.16          val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
    1.17          val import_segmentP = Parse.$$$ "import_segment" |-- import_segment
    1.18          val type_mapsP = Parse.$$$ "type_maps" |-- type_maps