--- 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;