--- a/src/HOL/Tools/datatype_realizer.ML Sun Nov 16 18:19:27 2008 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Sun Nov 16 20:03:42 2008 +0100
@@ -27,8 +27,7 @@
in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
fun prf_of thm =
- Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm)
- (Proofterm.proof_of (Thm.proof_of thm));
+ 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;