ProofContext.init;

--- a/src/HOL/Nominal/nominal_package.ML	Fri Nov 24 17:23:15 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Nov 24 22:05:12 2006 +0100
@@ -1549,7 +1549,7 @@
             val y = Free ("y", U);
             val y' = Free ("y'", U)
           in
-            standard (Goal.prove (Context.init_proof thy11) [] (finite_prems @
+            standard (Goal.prove (ProofContext.init thy11) [] (finite_prems @
                 [HOLogic.mk_Trueprop (R $ x $ y),
                  HOLogic.mk_Trueprop (HOLogic.mk_all ("y'", U,
                    HOLogic.mk_imp (R $ x $ y', HOLogic.mk_eq (y', y)))),
@@ -1652,7 +1652,7 @@
          Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT))))) dt_atomTs;
 
     val rec_unique_thms = split_conj_thm (Goal.prove
-      (Context.init_proof thy11) (map fst rec_unique_frees)
+      (ProofContext.init thy11) (map fst rec_unique_frees)
       (List.concat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems')
       (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls))
       (fn {prems, context} =>

--- a/src/HOL/Tools/datatype_codegen.ML	Fri Nov 24 17:23:15 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Nov 24 22:05:12 2006 +0100
@@ -380,13 +380,15 @@
   val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
   val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
   val not_eq_quodlibet = thm "not_eq_quodlibet";
-in fun get_cert_datatype thy dtco =
+in
+
+fun get_cert_datatype thy dtco =
   let
     val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
     val inject = (#inject o DatatypePackage.the_datatype thy) dtco
       |> map (fn thm => bool_eq_implies OF [thm] )
       |> map (Tactic.rewrite_rule [rew_eq, rew_conj]);
-    val ctxt = Context.init_proof thy;
+    val ctxt = ProofContext.init thy;
     val simpset = Simplifier.context ctxt
       (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
     val cos = map (fn (co, tys) =>
@@ -398,12 +400,15 @@
       |> map (fn t => Goal.prove_global thy [] [] t (K tac))
       |> map (fn thm => not_eq_quodlibet OF [thm])
   in inject @ distinct end
-end (*local*);
+
+end;
 
 local
   val not_sym = thm "HOL.not_sym";
   val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
-in fun get_eq_datatype thy dtco =
+in
+
+fun get_eq_datatype thy dtco =
   let
     val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
     fun mk_triv_inject co =
@@ -418,7 +423,7 @@
       in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
     val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
     val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
-    val ctxt = Context.init_proof thy;
+    val ctxt = ProofContext.init thy;
     val simpset = Simplifier.context ctxt
       (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
     val cos = map (fn (co, tys) =>
@@ -430,7 +435,8 @@
       |> map (fn t => Goal.prove_global thy [] [] t (K tac))
       |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
   in inject1 @ inject2 @ distinct end;
-end (*local*);
+
+end;
 
 fun add_datatype_case_const dtco thy =
   let

--- a/src/Provers/classical.ML	Fri Nov 24 17:23:15 2006 +0100
+++ b/src/Provers/classical.ML	Fri Nov 24 22:05:12 2006 +0100
@@ -888,7 +888,7 @@
 
 fun claset_of thy =
   let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
-  in context_cs (Context.init_proof thy) (! cs_ref) (ctxt_cs) end;
+  in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
 val claset = claset_of o Context.the_context;
 
 fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;

--- a/src/Pure/goal.ML	Fri Nov 24 17:23:15 2006 +0100
+++ b/src/Pure/goal.ML	Fri Nov 24 22:05:12 2006 +0100
@@ -106,7 +106,7 @@
 
 fun prove_multi ctxt xs asms props tac =
   let
-    val thy = Context.theory_of_proof ctxt;
+    val thy = ProofContext.theory_of ctxt;
     val string_of_term = Sign.string_of_term thy;
 
     fun err msg = cat_error msg
@@ -145,7 +145,7 @@
 fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
 
 fun prove_global thy xs asms prop tac =
-  Drule.standard (prove (Context.init_proof thy) xs asms prop (fn {prems, ...} => tac prems));
+  Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));
 
 
 

--- a/src/Pure/meta_simplifier.ML	Fri Nov 24 17:23:15 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Fri Nov 24 22:05:12 2006 +0100
@@ -366,7 +366,7 @@
 fun context ctxt =
   map_simpset1 (fn (rules, prems, bounds, _) => (rules, prems, bounds, SOME ctxt));
 
-val theory_context = context o Context.init_proof;
+val theory_context = context o ProofContext.init;
 
 fun fallback_context _ (ss as Simpset ({context = SOME _, ...}, _)) = ss
   | fallback_context thy ss =