removed redundant OuterLex.make_lexicon;

--- a/src/HOL/Import/import_syntax.ML	Fri Sep 14 22:22:53 2007 +0200
+++ b/src/HOL/Import/import_syntax.ML	Sat Sep 15 19:25:19 2007 +0200
@@ -157,7 +157,7 @@
 	val _ = TextIO.closeIn is
 	val orig_source = Source.of_string inp
 	val symb_source = Symbol.source false orig_source
-	val lexes = ref (OuterLex.make_lexicon ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"],
+	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

--- a/src/Pure/Isar/outer_lex.ML	Fri Sep 14 22:22:53 2007 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Sat Sep 15 19:25:19 2007 +0200
@@ -45,7 +45,6 @@
     (token, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
   val source_proper: (token, 'a) Source.source ->
     (token, (token, 'a) Source.source) Source.source
-  val make_lexicon: string list -> Scan.lexicon
 end;
 
 structure OuterLex: OUTER_LEX =
@@ -347,8 +346,4 @@
 fun source_proper src = src |> Source.filter is_proper;
 
 
-(* lexicons *)
-
-val make_lexicon = Scan.make_lexicon o map Symbol.explode;
-
 end;

--- a/src/Pure/Thy/thy_header.ML	Fri Sep 14 22:22:53 2007 +0200
+++ b/src/Pure/Thy/thy_header.ML	Sat Sep 15 19:25:19 2007 +0200
@@ -27,8 +27,8 @@
 val usesN = "uses";
 val beginN = "begin";
 
-val header_lexicon = T.make_lexicon
-  ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN];
+val header_lexicon = Scan.make_lexicon
+  (map Symbol.explode ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]);
 
 
 (* header args *)