src/Pure/Proof/proof_syntax.ML

       (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
   end;
 
 fun proof_of ctxt full raw_thm =
   let
-    val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm;
+    val thm = Thm.transfer' ctxt raw_thm;
     val prop = Thm.full_prop_of thm;
     val prf = Thm.proof_of thm;
     val prf' =
       (case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of
         (PThm (_, ((_, prop', _), body)), _) =>