--- a/src/HOL/Tools/datatype_realizer.ML Thu Apr 10 20:54:18 2008 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Sat Apr 12 17:00:35 2008 +0200
@@ -27,8 +27,7 @@
in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
fun prf_of thm =
- let val {thy, prop, der = (_, prf), ...} = rep_thm thm
- in Reconstruct.reconstruct_proof thy prop prf end;
+ Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
fun prf_subst_vars inst =
Proofterm.map_proof_terms (subst_vars ([], inst)) I;