src/Pure/Proof/proof_syntax.ML

       (map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names)
   end;
 
 fun proof_of full thm =
   let
-    val {thy, der = (_, prf), ...} = Thm.rep_thm thm;
+    val thy = Thm.theory_of_thm thm;
     val prop = Thm.full_prop_of thm;
+    val prf = Thm.proof_of thm;
     val prf' = (case strip_combt (fst (strip_combP prf)) of
         (PThm (_, prf', prop', _), _) => if prop = prop' then prf' else prf
       | _ => prf)
   in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;