# HG changeset patch
# User wenzelm
# Date 1184015564 -7200
# Node ID 1114cc909800f93107fe86d88522ca259b036242
# Parent  ea9b7e9c2301d8e1b157458107a1561ea9f27d6b
adapted OuterLex/T.source;

diff -r ea9b7e9c2301 -r 1114cc909800 src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Mon Jul 09 23:12:42 2007 +0200
+++ b/src/HOL/Import/import_syntax.ML	Mon Jul 09 23:12:44 2007 +0200
@@ -160,7 +160,7 @@
 	val lexes = ref (OuterLex.make_lexicon ["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 false get_lexes (Position.line 1) symb_source
+	val token_source = OuterLex.source NONE get_lexes (Position.line 1) 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
diff -r ea9b7e9c2301 -r 1114cc909800 src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Mon Jul 09 23:12:42 2007 +0200
+++ b/src/Pure/Isar/antiquote.ML	Mon Jul 09 23:12:44 2007 +0200
@@ -86,7 +86,7 @@
     val res =
       Source.of_string s
       |> Symbol.source false
-      |> T.source false (K (lex, Scan.empty_lexicon)) pos
+      |> T.source NONE (K (lex, Scan.empty_lexicon)) pos
       |> T.source_proper
       |> Source.source T.stopper (Scan.error (Scan.bulk antiq)) NONE
       |> Source.exhaust;
diff -r ea9b7e9c2301 -r 1114cc909800 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Mon Jul 09 23:12:42 2007 +0200
+++ b/src/Pure/Thy/thy_header.ML	Mon Jul 09 23:12:44 2007 +0200
@@ -53,7 +53,7 @@
   let val res =
     src
     |> Symbol.source false
-    |> T.source false (fn () => (header_lexicon, Scan.empty_lexicon)) pos
+    |> T.source NONE (fn () => (header_lexicon, Scan.empty_lexicon)) pos
     |> T.source_proper
     |> Source.source T.stopper (Scan.single (Scan.error header)) NONE
     |> Source.get_single;