src/HOL/Tools/record.ML

 
 fun future_forward_prf_standard thy prf prop () =
   let val thm =
     if ! quick_and_dirty then Skip_Proof.make_thm thy prop
     else if Goal.future_enabled () then
-      Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop
+      Goal.future_result (ProofContext.init_global thy) (Future.fork_pri ~1 prf) prop
     else prf ()
   in Drule.export_without_context thm end;
 
 fun prove_common immediate stndrd thy asms prop tac =
   let
     val prv =
       if ! quick_and_dirty then Skip_Proof.prove
       else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
       else Goal.prove_future;
-    val prf = prv (ProofContext.init thy) [] asms prop tac;
+    val prf = prv (ProofContext.init_global thy) [] asms prop tac;
   in if stndrd then Drule.export_without_context prf else prf end;
 
 val prove_future_global = prove_common false;
 val prove_global = prove_common true;
 

           if is_sel_upd_pair thy acc upd
           then mk_comp (Free ("f", T)) acc
           else mk_comp_id acc;
         val prop = lhs === rhs;
         val othm =
-          Goal.prove (ProofContext.init thy) [] [] prop
+          Goal.prove (ProofContext.init_global thy) [] [] prop
             (fn _ =>
               simp_tac defset 1 THEN
               REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
               TRY (simp_tac (HOL_ss addsimps id_o_apps) 1));
         val dest =

       if comp
       then u $ mk_comp f f'
       else mk_comp (u' $ f') (u $ f);
     val prop = lhs === rhs;
     val othm =
-      Goal.prove (ProofContext.init thy) [] [] prop
+      Goal.prove (ProofContext.init_global thy) [] [] prop
         (fn _ =>
           simp_tac defset 1 THEN
           REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
           TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
     val dest = if comp then o_eq_dest_lhs else o_eq_dest;

     val prop' = Envir.beta_eta_contract prop;
     val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
     val (_, args) = strip_comb lhs;
     val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
   in
-    Goal.prove (ProofContext.init thy) [] [] prop'
+    Goal.prove (ProofContext.init_global thy) [] [] prop'
       (fn _ =>
         simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
         TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
   end;
 

 fun get_upd_acc_cong_thm upd acc thy simpset =
   let
     val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)];
     val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
   in
-    Goal.prove (ProofContext.init thy) [] [] prop
+    Goal.prove (ProofContext.init_global thy) [] [] prop
       (fn _ =>
         simp_tac simpset 1 THEN
         REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
         TRY (resolve_tac [updacc_cong_idI] 1))
   end;

     val _ = Theory.requires thy "Record" "record definitions";
     val _ =
       if quiet_mode then ()
       else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
 
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     fun cert_typ T = Type.no_tvars (ProofContext.cert_typ ctxt T)
       handle TYPE (msg, _, _) => error msg;
 
 
     (* specification *)

   end
   handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
 
 fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
     val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
     val (parent, ctxt2) = read_parent raw_parent ctxt1;
     val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
     val params' = map (ProofContext.check_tfree ctxt3) params;