src/Pure/drule.ML

 
 fun ctyp_fun f cT =
   let val {T, thy, ...} = Thm.rep_ctyp cT
   in Thm.ctyp_of thy (f T) end;
 
-val cert = cterm_of ProtoPure.thy;
+val cert = cterm_of (Context.the_theory (Context.the_thread_data ()));
 
 val implies = cert Term.implies;
 fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B;
 
 (*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)

 
 
 
 (*** Meta-Rewriting Rules ***)
 
-val read_prop = Thm.cterm_of ProtoPure.thy o SimpleSyntax.read_prop;
+val read_prop = cert o SimpleSyntax.read_prop;
 
 fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
 fun store_standard_thm name thm = store_thm name (standard thm);
 fun store_thm_open name thm = hd (PureThy.smart_store_thms_open (name, [thm]));
 fun store_standard_thm_open name thm = store_thm_open name (standard' thm);

 
 (** protected propositions and embedded terms **)
 
 local
   val A = cert (Free ("A", propT));
-  val prop_def = Thm.unvarify ProtoPure.prop_def;
-  val term_def = Thm.unvarify ProtoPure.term_def;
+  val get_axiom = Thm.unvarify o Thm.get_axiom (Context.the_theory (Context.the_thread_data ()));
+  val prop_def = get_axiom "prop_def";
+  val term_def = get_axiom "term_def";
 in
   val protect = Thm.capply (cert Logic.protectC);
   val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
       (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
   val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard

   end;
 
 fun cterm_rule f = dest_term o f o mk_term;
 fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t));
 
-val dummy_thm = mk_term (Thm.cterm_of ProtoPure.thy (Term.dummy_pattern propT));
+val dummy_thm = mk_term (cert (Term.dummy_pattern propT));
 
 
 
 (** variations on instantiate **)