diff -r fda143b5c2f5 -r ae85c5d64913 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -270,7 +270,7 @@
 fun lemma thm ct =
   let
     val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
-    val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
+    val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm)
     val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
   in Thm (Z3_Proof_Tools.compose ccontr th) end
 end