# HG changeset patch
# User wenzelm
# Date 1237409738 -3600
# Node ID 49899f26fbd1014419fbab4221ad3faf87b6728d
# Parent  8fbc355100f2ffc29ff8e7b98b5a10584f18881a
de-camelized Symbol_Pos;

diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/General/symbol_pos.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -34,7 +34,7 @@
   val explode: text * Position.T -> T list
 end;
 
-structure SymbolPos: SYMBOL_POS =
+structure Symbol_Pos: SYMBOL_POS =
 struct
 
 (* type T *)
@@ -149,5 +149,5 @@
 
 end;
 
-structure BasicSymbolPos: BASIC_SYMBOL_POS = SymbolPos;   (*not open by default*)
+structure Basic_Symbol_Pos: BASIC_SYMBOL_POS = Symbol_Pos;   (*not open by default*)
 
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Isar/antiquote.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -7,12 +7,12 @@
 signature ANTIQUOTE =
 sig
   datatype antiquote =
-    Text of string | Antiq of SymbolPos.T list * Position.T |
+    Text of string | Antiq of Symbol_Pos.T list * Position.T |
     Open of Position.T | Close of Position.T
   val is_antiq: antiquote -> bool
-  val read: SymbolPos.T list * Position.T -> antiquote list
+  val read: Symbol_Pos.T list * Position.T -> antiquote list
   val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
-    SymbolPos.T list * Position.T -> 'a
+    Symbol_Pos.T list * Position.T -> 'a
 end;
 
 structure Antiquote: ANTIQUOTE =
@@ -22,7 +22,7 @@
 
 datatype antiquote =
   Text of string |
-  Antiq of SymbolPos.T list * Position.T |
+  Antiq of Symbol_Pos.T list * Position.T |
   Open of Position.T |
   Close of Position.T;
 
@@ -48,7 +48,7 @@
 
 (* scan_antiquote *)
 
-open BasicSymbolPos;
+open Basic_Symbol_Pos;
 structure T = OuterLex;
 
 local
@@ -63,18 +63,18 @@
   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
 
 val scan_antiq =
-  SymbolPos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
+  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
     T.!!! "missing closing brace of antiquotation"
-      (Scan.repeat scan_ant -- ($$$ "}" |-- SymbolPos.scan_pos)))
+      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
   >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
 
 in
 
 val scan_antiquote =
- (Scan.repeat1 scan_txt >> (Text o SymbolPos.content o flat) ||
+ (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
   scan_antiq ||
-  SymbolPos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
-  SymbolPos.scan_pos --| $$$ "\\<rbrace>" >> Close);
+  Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
+  Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
 
 end;
 
@@ -86,7 +86,7 @@
 
 fun read ([], _) = []
   | read (syms, pos) =
-      (case Scan.read SymbolPos.stopper (Scan.repeat scan_antiquote) syms of
+      (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
         SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
       | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
 
@@ -96,7 +96,7 @@
 fun read_antiq lex scan (syms, pos) =
   let
     fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
-      "@{" ^ SymbolPos.content syms ^ "}");
+      "@{" ^ Symbol_Pos.content syms ^ "}");
 
     val res =
       Source.of_list syms
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Isar/args.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -32,7 +32,7 @@
   val mode: string -> bool context_parser
   val maybe: 'a parser -> 'a option parser
   val name_source: string parser
-  val name_source_position: (SymbolPos.text * Position.T) parser
+  val name_source_position: (Symbol_Pos.text * Position.T) parser
   val name: string parser
   val binding: binding parser
   val alt_name: string parser
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -13,7 +13,7 @@
   val print_translation: bool * (string * Position.T) -> theory -> theory
   val typed_print_translation: bool * (string * Position.T) -> theory -> theory
   val print_ast_translation: bool * (string * Position.T) -> theory -> theory
-  val oracle: bstring * Position.T -> SymbolPos.text * Position.T -> theory -> theory
+  val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
   val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
   val declaration: string * Position.T -> local_theory -> local_theory
@@ -75,10 +75,10 @@
   val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
   val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
-  val header_markup: SymbolPos.text * Position.T -> Toplevel.transition -> Toplevel.transition
-  val local_theory_markup: xstring option * (SymbolPos.text * Position.T) ->
+  val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
+  val local_theory_markup: xstring option * (Symbol_Pos.text * Position.T) ->
     Toplevel.transition -> Toplevel.transition
-  val proof_markup: SymbolPos.text * Position.T -> Toplevel.transition -> Toplevel.transition
+  val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure IsarCmd: ISAR_CMD =
@@ -152,7 +152,7 @@
 
 fun oracle (name, pos) (body_txt, body_pos) =
   let
-    val body = SymbolPos.content (SymbolPos.explode (body_txt, body_pos));
+    val body = Symbol_Pos.content (Symbol_Pos.explode (body_txt, body_pos));
     val txt =
       "local\n\
       \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -35,7 +35,7 @@
   val is_blank: token -> bool
   val is_newline: token -> bool
   val source_of: token -> string
-  val source_position_of: token -> SymbolPos.text * Position.T
+  val source_position_of: token -> Symbol_Pos.text * Position.T
   val content_of: token -> string
   val unparse: token -> string
   val text_of: token -> string * string
@@ -50,14 +50,14 @@
   val assign: value option -> token -> unit
   val closure: token -> token
   val ident_or_symbolic: string -> bool
-  val !!! : string -> (SymbolPos.T list -> 'a) -> SymbolPos.T list -> 'a
-  val scan_quoted: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
+  val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
+  val scan_quoted: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
   val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
-    (SymbolPos.T, 'a) Source.source -> (token, (SymbolPos.T, 'a) Source.source) Source.source
+    (Symbol_Pos.T, 'a) Source.source -> (token, (Symbol_Pos.T, 'a) Source.source) Source.source
   val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
-      (SymbolPos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
+      (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
 end;
 
 structure OuterLex: OUTER_LEX =
@@ -92,7 +92,7 @@
   Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
   Malformed | Error of string | Sync | EOF;
 
-datatype token = Token of (SymbolPos.text * Position.range) * (token_kind * string) * slot;
+datatype token = Token of (Symbol_Pos.text * Position.range) * (token_kind * string) * slot;
 
 val str_of_kind =
  fn Command => "command"
@@ -259,9 +259,9 @@
 
 (** scanners **)
 
-open BasicSymbolPos;
+open Basic_Symbol_Pos;
 
-fun !!! msg = SymbolPos.!!! ("Outer lexical error: " ^ msg);
+fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
 
 fun change_prompt scan = Scan.prompt "# " scan;
 
@@ -303,8 +303,8 @@
   Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
 
 fun scan_strs q =
-  (SymbolPos.scan_pos --| $$$ q) -- !!! "missing quote at end of string"
-    (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- SymbolPos.scan_pos)));
+  (Symbol_Pos.scan_pos --| $$$ q) -- !!! "missing quote at end of string"
+    (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- Symbol_Pos.scan_pos)));
 
 in
 
@@ -323,8 +323,8 @@
   Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
 
 val scan_verbatim =
-  (SymbolPos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
-    (change_prompt ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- SymbolPos.scan_pos)));
+  (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
+    (change_prompt ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
 
 
 (* scan space *)
@@ -339,7 +339,7 @@
 (* scan comment *)
 
 val scan_comment =
-  SymbolPos.scan_pos -- (SymbolPos.scan_comment_body !!! -- SymbolPos.scan_pos);
+  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
 
 
 (* scan malformed symbols *)
@@ -360,10 +360,10 @@
 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
 
 fun token k ss =
-  Token ((SymbolPos.implode ss, SymbolPos.range ss), (k, SymbolPos.untabify_content ss), Slot);
+  Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
 
 fun token_range k (pos1, (ss, pos2)) =
-  Token (SymbolPos.implode_range pos1 pos2 ss, (k, SymbolPos.untabify_content ss), Slot);
+  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
 
 fun scan (lex1, lex2) = !!! "bad input"
   (scan_string >> token_range String ||
@@ -392,11 +392,11 @@
 in
 
 fun source' {do_recover} get_lex =
-  Source.source SymbolPos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
+  Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
     (Option.map (rpair recover) do_recover);
 
 fun source do_recover get_lex pos src =
-  SymbolPos.source pos src
+  Symbol_Pos.source pos src
   |> source' do_recover get_lex;
 
 end;
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -84,8 +84,8 @@
   val fixes: (binding * string option * mixfix) list parser
   val for_fixes: (binding * string option * mixfix) list parser
   val for_simple_fixes: (binding * string option) list parser
-  val ML_source: (SymbolPos.text * Position.T) parser
-  val doc_source: (SymbolPos.text * Position.T) parser
+  val ML_source: (Symbol_Pos.text * Position.T) parser
+  val doc_source: (Symbol_Pos.text * Position.T) parser
   val term_group: string parser
   val prop_group: string parser
   val term: string parser
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -224,7 +224,7 @@
 type isar =
   (Toplevel.transition, (Toplevel.transition option,
     (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
-      (SymbolPos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
+      (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
   Source.source) Source.source) Source.source) Source.source)
   Source.source) Source.source) Source.source) Source.source;
 
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -430,7 +430,7 @@
 
 local
 
-val token_content = Syntax.read_token #>> SymbolPos.content;
+val token_content = Syntax.read_token #>> Symbol_Pos.content;
 
 fun prep_const_proper ctxt (c, pos) =
   let val t as (Const (d, _)) =
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -191,12 +191,12 @@
 
 fun eval_antiquotes (txt, pos) opt_context =
   let
-    val syms = SymbolPos.explode (txt, pos);
+    val syms = Symbol_Pos.explode (txt, pos);
     val ants = Antiquote.read (syms, pos);
     val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
     val ((ml_env, ml_body), opt_ctxt') =
       if not (exists Antiquote.is_antiq ants)
-      then (("", Symbol.escape (SymbolPos.content syms)), opt_ctxt)
+      then (("", Symbol.escape (Symbol_Pos.content syms)), opt_ctxt)
       else
         let
           val ctxt =
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -18,7 +18,7 @@
   val content_of: token -> string
   val keywords: string list
   val source: (Symbol.symbol, 'a) Source.source ->
-    (token, (SymbolPos.T, Position.T * (Symbol.symbol, 'a) Source.source)
+    (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
       Source.source) Source.source
 end;
 
@@ -75,9 +75,9 @@
 
 (** scanners **)
 
-open BasicSymbolPos;
+open Basic_Symbol_Pos;
 
-fun !!! msg = SymbolPos.!!! ("SML lexical error: " ^ msg);
+fun !!! msg = Symbol_Pos.!!! ("SML lexical error: " ^ msg);
 
 
 (* blanks *)
@@ -183,13 +183,13 @@
 
 local
 
-fun token k ss = Token (SymbolPos.range ss, (k, SymbolPos.implode ss));
+fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.implode ss));
 
 val scan = !!! "bad input"
  (scan_char >> token Char ||
   scan_string >> token String ||
   scan_blanks1 >> token Space ||
-  SymbolPos.scan_comment !!! >> token Comment ||
+  Symbol_Pos.scan_comment !!! >> token Comment ||
   Scan.max token_leq
    (scan_keyword >> token Keyword)
    (scan_word >> token Word ||
@@ -206,8 +206,8 @@
 in
 
 fun source src =
-  SymbolPos.source (Position.line 1) src
-  |> Source.source SymbolPos.stopper (Scan.bulk scan) (SOME (false, recover));
+  Symbol_Pos.source (Position.line 1) src
+  |> Source.source Symbol_Pos.stopper (Scan.bulk scan) (SOME (false, recover));
 
 end;
 
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);
 
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -21,7 +21,7 @@
 
 fun read scan s =
   (case
-      SymbolPos.explode (s, Position.none) |>
+      Symbol_Pos.explode (s, Position.none) |>
       Lexicon.tokenize lexicon false |>
       filter Lexicon.is_proper |>
       Scan.read Lexicon.stopper scan of
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -35,7 +35,7 @@
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
   val guess_infix: syntax -> string -> mixfix option
-  val read_token: string -> SymbolPos.T list * Position.T
+  val read_token: string -> Symbol_Pos.T list * Position.T
   val ambiguity_is_error: bool ref
   val ambiguity_level: int ref
   val ambiguity_limit: int ref
@@ -43,12 +43,12 @@
     (((string * int) * sort) list -> string * int -> Term.sort) ->
     (string -> bool * string) -> (string -> string option) ->
     (typ -> typ) -> (sort -> sort) -> Proof.context ->
-    (string -> bool) -> syntax -> typ -> SymbolPos.T list * Position.T -> term
+    (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
   val standard_parse_typ: Proof.context -> syntax ->
     ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
-    SymbolPos.T list * Position.T -> typ
+    Symbol_Pos.T list * Position.T -> typ
   val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) ->
-    SymbolPos.T list * Position.T -> sort
+    Symbol_Pos.T list * Position.T -> sort
   datatype 'a trrule =
     ParseRule of 'a * 'a |
     PrintRule of 'a * 'a |
@@ -82,7 +82,7 @@
     (string * string) trrule list -> syntax -> syntax
   val update_trrules_i: ast trrule list -> syntax -> syntax
   val remove_trrules_i: ast trrule list -> syntax -> syntax
-  val parse_token: Markup.T -> string -> SymbolPos.T list * Position.T
+  val parse_token: Markup.T -> string -> Symbol_Pos.T list * Position.T
   val parse_sort: Proof.context -> string -> sort
   val parse_typ: Proof.context -> string -> typ
   val parse_term: Proof.context -> string -> term
@@ -467,7 +467,7 @@
     | XML.Elem ("token", props, []) => ("", Position.of_properties props)
     | XML.Text text => (text, Position.none)
     | _ => (str, Position.none))
-  in (SymbolPos.explode (text, pos), pos) end;
+  in (Symbol_Pos.explode (text, pos), pos) end;
 
 
 (* read_ast *)
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Thy/latex.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -90,7 +90,7 @@
 val output_syms_antiq =
   (fn Antiquote.Text s => output_syms s
     | Antiquote.Antiq (ss, _) =>
-        enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map SymbolPos.symbol ss))
+        enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
     | Antiquote.Open _ => "{\\isaantiqopen}"
     | Antiquote.Close _ => "{\\isaantiqclose}");
 
@@ -117,7 +117,7 @@
     else if T.is_kind T.Verbatim tok then
       let
         val (txt, pos) = T.source_position_of tok;
-        val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
+        val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
         val out = implode (map output_syms_antiq ants);
       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
     else output_syms s
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -22,7 +22,7 @@
     ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
   datatype markup = Markup | MarkupEnv | Verbatim
   val modes: string list ref
-  val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
+  val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
   val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
   val pretty_text: string -> Pretty.T
@@ -156,7 +156,7 @@
           end
       | expand (Antiquote.Open _) = ""
       | expand (Antiquote.Close _) = "";
-    val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
+    val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
   in
     if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
       error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
@@ -577,7 +577,7 @@
 fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
   (fn {context, ...} => fn (txt, pos) =>
    (ML_Context.eval_in (SOME context) false pos (ml txt);
-    SymbolPos.content (SymbolPos.explode (txt, pos))
+    Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
     |> (if ! quotes then quote else I)
     |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
     else
diff -r 8fbc355100f2 -r 49899f26fbd1 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Mar 18 21:55:38 2009 +0100
@@ -7,7 +7,7 @@
 signature THY_SYNTAX =
 sig
   val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
-    (OuterLex.token, (SymbolPos.T, Position.T * (Symbol.symbol, (string, 'a)
+    (OuterLex.token, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
       Source.source) Source.source) Source.source) Source.source
   val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list
   val present_token: OuterLex.token -> output