# HG changeset patch
# User wenzelm
# Date 1226781077 -3600
# Node ID ee65e7d043fcda05452093d260fc2fe6f466354a
# Parent  a0dd52dd7b55d2ba35d92eb2da1e602771fbb6ca
Thm.proof_of returns proof_body;

diff -r a0dd52dd7b55 -r ee65e7d043fc src/HOL/Tools/datatype_realizer.ML
--- 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;
diff -r a0dd52dd7b55 -r ee65e7d043fc src/Pure/Isar/isar_cmd.ML
--- 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