# HG changeset patch
# User wenzelm
# Date 1218129697 -7200
# Node ID a9d16f8b997a29978f2a3bc152a78cca776a0ef3
# Parent  51c7b1baaf35f04a360262e18220c0c6d62320c9
Position.start;

diff -r 51c7b1baaf35 -r a9d16f8b997a src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Thu Aug 07 13:45:15 2008 +0200
+++ b/src/HOL/Import/import_syntax.ML	Thu Aug 07 19:21:37 2008 +0200
@@ -160,7 +160,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"]),
 			 Scan.empty_lexicon)
 	val get_lexes = fn () => !lexes
-	val token_source = OuterLex.source NONE get_lexes (Position.line 1) symb_source
+	val token_source = OuterLex.source NONE get_lexes Position.start symb_source
 	val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)
 	val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
 	val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps