--- a/src/HOL/Tools/datatype_realizer.ML Sat Nov 15 21:31:15 2008 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Sat Nov 15 21:31:17 2008 +0100
@@ -27,7 +27,8 @@
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) (Thm.proof_of thm);
+ Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm)
+ (Proofterm.proof_of (Thm.proof_of thm));
fun prf_subst_vars inst =
Proofterm.map_proof_terms (subst_vars ([], inst)) I;
--- a/src/Pure/Isar/isar_cmd.ML Sat Nov 15 21:31:15 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sat Nov 15 21:31:17 2008 +0100
@@ -469,7 +469,7 @@
let
val (ctxt, (_, thm)) = Proof.get_goal state;
val thy = ProofContext.theory_of ctxt;
- val prf = Thm.proof_of thm;
+ val prf = Proofterm.proof_of (Thm.proof_of thm);
val prop = Thm.full_prop_of thm;
val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
in