src/HOL/Import/import_syntax.ML
changeset 32740 9dd0a2f83429
parent 27835 ff8b8513965a
child 32960 69916a850301
     1.1 --- a/src/HOL/Import/import_syntax.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -157,8 +157,9 @@
     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 = 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"]),
     1.8 -			 Scan.empty_lexicon)
     1.9 +	val lexes = Unsynchronized.ref
    1.10 +	  (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.11 +		  Scan.empty_lexicon)
    1.12  	val get_lexes = fn () => !lexes
    1.13  	val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source
    1.14  	val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)