# HG changeset patch
# User wenzelm
# Date 1282919531 -7200
# Node ID 38b68972721bbe0abe5f8cf127a170a9fe6515da
# Parent  a925c0ee42f779e3e419c2f9ce317b7acb8a6384
eliminated unnecessary ref;

diff -r a925c0ee42f7 -r 38b68972721b src/HOL/Import/import_syntax.ML
--- 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