# HG changeset patch
# User wenzelm
# Date 1237459909 -3600
# Node ID b51811144ed4317faae62e2d2506165065405c92
# Parent  638b088bb84076eced4df06a90fd4c5e4a2a4980# Parent  4169ddbfe1f9ceb87365c380fe8a2609740cfe4b
merged

diff -r 638b088bb840 -r b51811144ed4 NEWS
--- a/NEWS	Thu Mar 19 01:29:19 2009 -0700
+++ b/NEWS	Thu Mar 19 11:51:49 2009 +0100
@@ -176,30 +176,28 @@
 * The 'axiomatization' command now only works within a global theory
 context.  INCOMPATIBILITY.
 
-* New find_theorems criterion "solves" matching theorems that directly
-solve the current goal. Try "find_theorems solves".
-
-* Added an auto solve option, which can be enabled through the
-ProofGeneral Isabelle settings menu (disabled by default).
- 
-When enabled, find_theorems solves is called whenever a new lemma is
-stated. Any theorems that could solve the lemma directly are listed
-underneath the goal.
-
-* New command 'find_consts' searches for constants based on type and
-name patterns, e.g.
+* New 'find_theorems' criterion "solves" matching theorems that
+directly solve the current goal.
+
+* Auto solve feature for main theorem statements (cf. option in Proof
+General Isabelle settings menu, enabled by default).  Whenever a new
+goal is stated, "find_theorems solves" is called; any theorems that
+could solve the lemma directly are listed underneath the goal.
+
+* Command 'find_consts' searches for constants based on type and name
+patterns, e.g.
 
     find_consts "_ => bool"
 
 By default, matching is against subtypes, but it may be restricted to
-the whole type. Searching by name is possible. Multiple queries are
+the whole type. Searching by name is possible.  Multiple queries are
 conjunctive and queries may be negated by prefixing them with a
 hyphen:
 
     find_consts strict: "_ => bool" name: "Int" -"int => int"
 
-* New command 'local_setup' is similar to 'setup', but operates on a
-local theory context.
+* Command 'local_setup' is similar to 'setup', but operates on a local
+theory context.
 
 
 *** Document preparation ***
diff -r 638b088bb840 -r b51811144ed4 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/General/symbol_pos.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/antiquote.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/args.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/attrib.ML	Thu Mar 19 11:51:49 2009 +0100
@@ -26,7 +26,8 @@
   val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
   val syntax: attribute context_parser -> src -> attribute
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
-  val attribute_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
+  val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
+    theory -> theory
   val no_args: attribute -> src -> attribute
   val add_del: attribute -> attribute -> attribute context_parser
   val add_del_args: attribute -> attribute -> src -> attribute
diff -r 638b088bb840 -r b51811144ed4 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 19 11:51:49 2009 +0100
@@ -6,18 +6,18 @@
 
 signature ISAR_CMD =
 sig
-  val global_setup: string * Position.T -> theory -> theory
-  val local_setup: string * Position.T -> Proof.context -> Proof.context
-  val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
-  val parse_translation: bool * (string * Position.T) -> theory -> theory
-  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 global_setup: Symbol_Pos.text * Position.T -> theory -> theory
+  val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
+  val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val print_ast_translation: bool * (Symbol_Pos.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
-  val simproc_setup: string -> string list -> string * Position.T -> string list ->
+  val declaration: Symbol_Pos.text * Position.T -> local_theory -> local_theory
+  val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
     local_theory -> local_theory
   val hide_names: bool -> string * xstring list -> theory -> theory
   val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
@@ -38,7 +38,7 @@
   val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
   val disable_pr: Toplevel.transition -> Toplevel.transition
   val enable_pr: Toplevel.transition -> Toplevel.transition
-  val ml_diag: bool -> string * Position.T -> Toplevel.transition -> Toplevel.transition
+  val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
@@ -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 638b088bb840 -r b51811144ed4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 19 11:51:49 2009 +0100
@@ -272,7 +272,7 @@
   OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
 
 val _ =
-  OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
+  OuterSyntax.local_theory "declare" "declare theorems" K.thy_decl
     (P.and_list1 SpecParse.xthms1
       >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
 
@@ -295,28 +295,35 @@
 
 (* use ML text *)
 
+fun inherit_env (context as Context.Proof lthy) =
+      Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
+  | inherit_env context = context;
+
+fun inherit_env_prf prf = Proof.map_contexts
+  (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
+
 val _ =
-  OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.thy_decl)
-    (P.path >> (Toplevel.generic_theory o ThyInfo.exec_file false));
+  OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
+    (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> inherit_env)));
 
 val _ =
-  OuterSyntax.command "ML" "eval ML text within theory" (K.tag_ml K.thy_decl)
+  OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl)
     (P.ML_source >> (fn (txt, pos) =>
-      Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
+      Toplevel.generic_theory
+        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env)));
 
 val _ =
-  OuterSyntax.command "ML_prf" "eval ML text within proof" (K.tag_proof K.prf_decl)
+  OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl)
     (P.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #>
-          (fn prf => Proof.map_contexts (ML_Context.inherit_env (Proof.context_of prf)) prf))));
+        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)));
 
 val _ =
-  OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
+  OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag)
     (P.ML_source >> IsarCmd.ml_diag true);
 
 val _ =
-  OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag)
+  OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (K.tag_ml K.diag)
     (P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
 
 val _ =
diff -r 638b088bb840 -r b51811144ed4 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/local_theory.ML	Thu Mar 19 11:51:49 2009 +0100
@@ -23,6 +23,7 @@
   val theory: (theory -> theory) -> local_theory -> local_theory
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
+  val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
   val affirm: local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
@@ -163,6 +164,11 @@
 
 fun target f = #2 o target_result (f #> pair ());
 
+fun map_contexts f =
+  theory (Context.theory_map f) #>
+  target (Context.proof_map f) #>
+  Context.proof_map f;
+
 
 (* basic operations *)
 
diff -r 638b088bb840 -r b51811144ed4 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/method.ML	Thu Mar 19 11:51:49 2009 +0100
@@ -81,7 +81,8 @@
     -> theory -> theory
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
-  val method_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
+  val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
+    theory -> theory
   val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
   val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
   val no_args: method -> src -> Proof.context -> method
diff -r 638b088bb840 -r b51811144ed4 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/outer_lex.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/outer_parse.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 19 11:51:49 2009 +0100
@@ -19,7 +19,7 @@
   val the_global_context: unit -> theory
   val the_local_context: unit -> Proof.context
   val exec: (unit -> unit) -> Context.generic -> Context.generic
-  val inherit_env: Proof.context -> Proof.context -> Proof.context
+  val inherit_env: Context.generic -> Context.generic -> Context.generic
   val name_space: ML_NameSpace.nameSpace
   val stored_thms: thm list ref
   val ml_store_thm: string * thm -> unit
@@ -29,10 +29,11 @@
       (Proof.context -> string * string) * Proof.context
   val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
   val trace: bool ref
-  val eval_wrapper: (string -> unit) * (string -> 'a) -> bool -> Position.T -> string -> unit
-  val eval: bool -> Position.T -> string -> unit
+  val eval_wrapper: (string -> unit) * (string -> 'a) -> bool ->
+    Position.T -> Symbol_Pos.text -> unit
+  val eval: bool -> Position.T -> Symbol_Pos.text -> unit
   val eval_file: Path.T -> unit
-  val eval_in: Proof.context option -> bool -> Position.T -> string -> unit
+  val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
   val evaluate: Proof.context -> (string -> unit) * (string -> 'b) -> bool ->
     string * (unit -> 'a) option ref -> string -> 'a
   val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
@@ -77,7 +78,7 @@
     Symtab.merge (K true) (functor1, functor2));
 );
 
-val inherit_env = Context.proof_map o ML_Env.put o ML_Env.get o Context.Proof;
+val inherit_env = ML_Env.put o ML_Env.get;
 
 val name_space: ML_NameSpace.nameSpace =
   let
@@ -191,12 +192,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 638b088bb840 -r b51811144ed4 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/ML/ml_lex.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Syntax/lexicon.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Syntax/simple_syntax.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Syntax/syntax.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Thy/latex.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 19 11:51:49 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 638b088bb840 -r b51811144ed4 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Thy/thy_syntax.ML	Thu Mar 19 11:51:49 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