diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -9,15 +9,15 @@
   val is_identifier: string -> bool
   val is_ascii_identifier: string -> bool
   val is_tid: string -> bool
-  val scan_id: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
-  val scan_longid: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
-  val scan_tid: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
-  val scan_nat: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
-  val scan_int: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
-  val scan_hex: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
-  val scan_bin: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
-  val scan_var: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
-  val scan_tvar: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
+  val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val implode_xstr: string list -> string
   val explode_xstr: string -> string list
   val read_indexname: string -> indexname
@@ -60,7 +60,7 @@
   val matching_tokens: token * token -> bool
   val valued_token: token -> bool
   val predef_term: string -> token option
-  val tokenize: Scan.lexicon -> bool -> SymbolPos.T list -> token list
+  val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
 end;
 
 structure Lexicon: LEXICON =
@@ -88,9 +88,9 @@
 
 (** basic scanners **)
 
-open BasicSymbolPos;
+open Basic_Symbol_Pos;
 
-fun !!! msg = SymbolPos.!!! ("Inner lexical error: " ^ msg);
+fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg);
 
 val scan_id = Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
 val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
@@ -220,7 +220,7 @@
 fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
 
 fun explode_xstr str =
-  (case Scan.read SymbolPos.stopper scan_str_body (SymbolPos.explode (str, Position.none)) of
+  (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
     SOME cs => map symbol cs
   | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
 
@@ -229,7 +229,7 @@
 (** tokenize **)
 
 fun token_leq (Token (_, s1, _), Token (_, s2, _)) = s1 <= s2;
-fun token kind ss = Token (kind, SymbolPos.content ss, SymbolPos.range ss);
+fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss);
 
 fun tokenize lex xids syms =
   let
@@ -252,16 +252,16 @@
     val scan_lit = Scan.literal lex >> token Literal;
 
     val scan_token =
-      SymbolPos.scan_comment !!! >> token Comment ||
+      Symbol_Pos.scan_comment !!! >> token Comment ||
       Scan.max token_leq scan_lit scan_val ||
       scan_str >> token StrSy ||
       Scan.many1 (Symbol.is_blank o symbol) >> token Space;
   in
     (case Scan.error
-        (Scan.finite SymbolPos.stopper (Scan.repeat scan_token)) syms of
+        (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
       (toks, []) => toks
-    | (_, ss) => error ("Inner lexical error at: " ^ SymbolPos.content ss ^
-        Position.str_of (#1 (SymbolPos.range ss))))
+    | (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^
+        Position.str_of (#1 (Symbol_Pos.range ss))))
   end;
 
 
@@ -303,7 +303,7 @@
 (* indexname *)
 
 fun read_indexname s =
-  (case Scan.read SymbolPos.stopper scan_indexname (SymbolPos.explode (s, Position.none)) of
+  (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode (s, Position.none)) of
     SOME xi => xi
   | _ => error ("Lexical error in variable name: " ^ quote s));
 
@@ -317,16 +317,16 @@
 fun read_var str =
   let
     val scan =
-      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one SymbolPos.is_eof) >> var ||
+      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var ||
       Scan.many (Symbol.is_regular o symbol) >> (free o implode o map symbol);
-  in the (Scan.read SymbolPos.stopper scan (SymbolPos.explode (str, Position.none))) end;
+  in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
 
 
 (* read_variable *)
 
 fun read_variable str =
   let val scan = $$$ "?" |-- scan_indexname || scan_indexname
-  in Scan.read SymbolPos.stopper scan (SymbolPos.explode (str, Position.none)) end;
+  in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
 
 
 (* specific identifiers *)
@@ -341,14 +341,14 @@
 
 fun nat cs =
   Option.map (#1 o Library.read_int o map symbol)
-    (Scan.read SymbolPos.stopper scan_nat cs);
+    (Scan.read Symbol_Pos.stopper scan_nat cs);
 
 in
 
-fun read_nat s = nat (SymbolPos.explode (s, Position.none));
+fun read_nat s = nat (Symbol_Pos.explode (s, Position.none));
 
 fun read_int s =
-  (case SymbolPos.explode (s, Position.none) of
+  (case Symbol_Pos.explode (s, Position.none) of
     ("-", _) :: cs => Option.map ~ (nat cs)
   | cs => nat cs);