diff -r e0cc4169626e -r c6231d64d264 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Apr 10 20:54:18 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Sat Apr 12 17:00:35 2008 +0200
@@ -711,7 +711,9 @@
 
     fun prep_thm (thm, vs) =
       let
-        val {prop, der = (_, prf), thy, ...} = rep_thm thm;
+        val thy = Thm.theory_of_thm thm;
+        val prop = Thm.prop_of thm;
+        val prf = Thm.proof_of thm;
         val name = Thm.get_name thm;
         val _ = name <> "" orelse error "extraction: unnamed theorem";
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^