clarified modules -- simplified bootstrap;

--- a/src/Doc/Implementation/ML.thy	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Doc/Implementation/ML.thy	Tue Apr 05 20:03:24 2016 +0200
@@ -616,15 +616,15 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
+  @{index_ML Context.the_generic_context: "unit -> Context.generic"} \\
   @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
   @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
   @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
   \end{mldecls}
 
-    \<^descr> @{ML "ML_Context.the_generic_context ()"} refers to the theory context of
+    \<^descr> @{ML "Context.the_generic_context ()"} refers to the theory context of
     the ML toplevel --- at compile time. ML code needs to take care to refer to
-    @{ML "ML_Context.the_generic_context ()"} correctly. Recall that evaluation
+    @{ML "Context.the_generic_context ()"} correctly. Recall that evaluation
     of a function body is delayed until actual run-time.
 
     \<^descr> @{ML "Context.>>"}~\<open>f\<close> applies context transformation \<open>f\<close> to the implicit

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -280,7 +280,7 @@
                   val output_value = the_default "NONE"
                     (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
                   val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
-                    ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
+                    ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))";
                   val ctxt' = ctxt
                     |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
                     |> Context.proof_map (exec false ml_code);

--- a/src/Pure/Isar/outer_syntax.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -120,7 +120,7 @@
         NONE => ()
       | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
     val _ =
-      Context_Position.report_generic (ML_Context.the_generic_context ())
+      Context_Position.report_generic (Context.the_generic_context ())
         (command_pos cmd) (command_markup true (name, cmd));
   in Data.map (Symtab.update (name, cmd)) thy end;
 

--- a/src/Pure/ML/ml_context.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -6,9 +6,6 @@
 
 signature ML_CONTEXT =
 sig
-  val the_generic_context: unit -> Context.generic
-  val the_global_context: unit -> theory
-  val the_local_context: unit -> Proof.context
   val thm: xstring -> thm
   val thms: xstring -> thm list
   val exec: (unit -> unit) -> Context.generic -> Context.generic
@@ -35,12 +32,8 @@
 
 (** implicit ML context **)
 
-val the_generic_context = Context.the_thread_data;
-val the_global_context = Context.theory_of o the_generic_context;
-val the_local_context = Context.proof_of o the_generic_context;
-
-fun thm name = Proof_Context.get_thm (the_local_context ()) name;
-fun thms name = Proof_Context.get_thms (the_local_context ()) name;
+fun thm name = Proof_Context.get_thm (Context.the_local_context ()) name;
+fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name;
 
 fun exec (e: unit -> unit) context =
   (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
@@ -123,7 +116,7 @@
   (ML_Lex.tokenize
     ("structure " ^ name ^ " =\nstruct\n\
      \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
-     " (ML_Context.the_local_context ());\n\
+     " (Context.the_local_context ());\n\
      \val ML_print_depth =\n\
      \  let val default = ML_Options.get_print_depth ()\n\
      \  in fn () => ML_Options.get_print_depth_default default end;\n"),
@@ -233,7 +226,7 @@
     eval ML_Compiler.flags (#1 range)
      (ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @
       ML_Lex.read (": " ^ constraint ^ " =") @ ants @
-      ML_Lex.read ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
+      ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
 
 end;
 

--- a/src/Pure/ML/ml_env.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -130,7 +130,7 @@
   let
     fun lookup sel1 sel2 name =
       if SML then
-        Context.the_thread_data ()
+        Context.the_generic_context ()
         |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
       else
         Context.thread_data ()
@@ -139,7 +139,7 @@
 
     fun all sel1 sel2 () =
       (if SML then
-        Context.the_thread_data ()
+        Context.the_generic_context ()
         |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
       else
         Context.thread_data ()

--- a/src/Pure/ML/ml_thms.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/ML/ml_thms.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -113,7 +113,7 @@
   fun merge _ = [];
 );
 
-fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ());
+fun get_stored_thms () = Stored_Thms.get (Context.the_global_context ());
 val get_stored_thm = hd o get_stored_thms;
 
 fun ml_store get (name, ths) =

--- a/src/Pure/Thy/thy_info.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -260,7 +260,7 @@
     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
       Resources.load_thy document symbols last_timing update_time dir header text_pos text
-        (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
+        (if name = Context.PureN then [Context.the_global_context ()] else parents);
     fun commit () = update_thy deps theory;
   in
     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}

--- a/src/Pure/Tools/debugger.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -155,7 +155,7 @@
 
 fun eval_context thread_name index SML toks =
   let
-    val context = ML_Context.the_generic_context ();
+    val context = Context.the_generic_context ();
     val context1 =
       if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
       then context

--- a/src/Pure/conjunction.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/conjunction.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -30,7 +30,7 @@
 
 (** abstract syntax **)
 
-fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
+fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
 val read_prop = certify o Simple_Syntax.read_prop;
 
 val true_prop = certify Logic.true_prop;
@@ -76,7 +76,7 @@
 val A_B = read_prop "A &&& B";
 
 val conjunction_def =
-  Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def";
+  Thm.unvarify_axiom (Context.the_global_context ()) "Pure.conjunction_def";
 
 fun conjunctionD which =
   Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
@@ -137,7 +137,7 @@
 
 local
 
-val bootstrap_thy = Context.theory_of (Context.the_thread_data ());
+val bootstrap_thy = Context.the_global_context ();
 
 fun conjs n =
   let

--- a/src/Pure/context.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/context.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -74,9 +74,11 @@
   val proof_of: generic -> Proof.context  (*total*)
   (*thread data*)
   val thread_data: unit -> generic option
-  val the_thread_data: unit -> generic
   val set_thread_data: generic option -> unit
   val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
+  val the_generic_context: unit -> generic
+  val the_global_context: unit -> theory
+  val the_local_context: unit -> Proof.context
   val >> : (generic -> generic) -> unit
   val >>> : (generic -> 'a * generic) -> 'a
 end;
@@ -496,19 +498,22 @@
     SOME (SOME context) => SOME context
   | _ => NONE);
 
-fun the_thread_data () =
+fun set_thread_data context = Thread.setLocal (tag, context);
+fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
+
+fun the_generic_context () =
   (case thread_data () of
     SOME context => context
   | _ => error "Unknown context");
 
-fun set_thread_data context = Thread.setLocal (tag, context);
-fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
+val the_global_context = theory_of o the_generic_context;
+val the_local_context = proof_of o the_generic_context;
 
 end;
 
 fun >>> f =
   let
-    val (res, context') = f (the_thread_data ());
+    val (res, context') = f (the_generic_context ());
     val _ = set_thread_data (SOME context');
   in res end;
 

--- a/src/Pure/drule.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/drule.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -134,7 +134,7 @@
 (*The premises of a theorem, as a cterm list*)
 val cprems_of = strip_imp_prems o Thm.cprop_of;
 
-fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
+fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
 
 val implies = certify Logic.implies;
 fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B;
@@ -570,7 +570,7 @@
 
 local
   val A = certify (Free ("A", propT));
-  val axiom = Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ()));
+  val axiom = Thm.unvarify_axiom (Context.the_global_context ());
   val prop_def = axiom "Pure.prop_def";
   val term_def = axiom "Pure.term_def";
   val sort_constraint_def = axiom "Pure.sort_constraint_def";
@@ -645,7 +645,7 @@
   store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
     (Thm.equal_intr
       (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
-        (Thm.unvarify_global (Context.the_theory (Context.the_thread_data ())) sort_constraintI)))
+        (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
       (implies_intr_list [A, C] (Thm.assume A)));
 
 end;

--- a/src/Pure/pure_syn.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/pure_syn.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -55,7 +55,7 @@
       (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
 
 
-val bootstrap_thy = ML_Context.the_global_context ();
+val bootstrap_thy = Context.the_global_context ();
 
 val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
 

--- a/src/Pure/raw_simplifier.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -1392,11 +1392,10 @@
   Variable.gen_all ctxt;
 
 val hhf_ss =
-  simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
-    addsimps Drule.norm_hhf_eqs);
+  simpset_of (empty_simpset (Context.the_local_context ()) addsimps Drule.norm_hhf_eqs);
 
 val hhf_protect_ss =
-  simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
+  simpset_of (empty_simpset (Context.the_local_context ())
     addsimps Drule.norm_hhf_eqs |> add_eqcong Drule.protect_cong);
 
 in

--- a/src/Tools/Code/code_runtime.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -88,7 +88,7 @@
   let
     val code = (prelude
       ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
-      ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
+      ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))");
     val ctxt' = ctxt
       |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
       |> Context.proof_map (exec ctxt false code);
@@ -539,7 +539,7 @@
       ML_Compiler0.use_text notifying_context
         {line = 0, file = Path.implode filepath, verbose = false, debug = false}
         (File.read filepath);
-    val thy'' = Context.the_theory (Context.the_thread_data ());
+    val thy'' = Context.the_global_context ();
     val names = Loaded_Values.get thy'';
   in (names, thy'') end;
 

--- a/src/Tools/Spec_Check/gen_construction.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Tools/Spec_Check/gen_construction.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -155,7 +155,7 @@
 
 (*produce compilable string*)
 fun build_check ctxt name (ty, spec) =
-  "Spec_Check.checkGen (ML_Context.the_local_context ()) ("
+  "Spec_Check.checkGen (Context.the_local_context ()) ("
   ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
   ^ name ^ "\", Property.pred (" ^ spec ^ "));";
 

--- a/src/Tools/Spec_Check/spec_check.ML	Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Tools/Spec_Check/spec_check.ML	Tue Apr 05 20:03:24 2016 +0200
@@ -192,5 +192,5 @@
 
 end;
 
-fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s;
+fun check_property s = Spec_Check.check_property (Context.the_local_context ()) s;