diff -r e0cc4169626e -r c6231d64d264 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 10 20:54:18 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Apr 12 17:00:35 2008 +0200
@@ -359,7 +359,8 @@
 
     fun mk_funs_inv thm =
       let
-        val {thy, prop, ...} = rep_thm thm;
+        val thy = Thm.theory_of_thm thm;
+        val prop = Thm.prop_of thm;
         val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
           (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
         val used = add_term_tfree_names (a, []);