src/Pure/drule.ML

   | _ => ct);
 
 (*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;
 
 (*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)

 
 (** embedded terms and types **)
 
 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";
   val C = Thm.lhs_of sort_constraint_def;
   val T = Thm.dest_arg C;

 
 val sort_constraint_eq =
   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;