--- a/src/Pure/drule.ML Tue Jul 28 21:31:16 2015 +0200
+++ b/src/Pure/drule.ML Tue Jul 28 21:47:03 2015 +0200
@@ -566,7 +566,7 @@
local
val A = certify (Free ("A", propT));
- val axiom = Thm.unvarify_global o Thm.axiom (Context.the_theory (Context.the_thread_data ()));
+ val axiom = Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ()));
val prop_def = axiom "Pure.prop_def";
val term_def = axiom "Pure.term_def";
val sort_constraint_def = axiom "Pure.sort_constraint_def";
@@ -640,7 +640,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 sort_constraintI)))
+ (Thm.unvarify_global (Context.the_theory (Context.the_thread_data ())) sort_constraintI)))
(implies_intr_list [A, C] (Thm.assume A)));
end;