diff --git a/src/Pure/thm.ML b/src/Pure/thm.ML
--- a/src/Pure/thm.ML
+++ b/src/Pure/thm.ML
@@ -833,7 +833,7 @@
     val Thm (Deriv {promises, ...}, {cert, constraints, shyps, hyps, tpairs, prop, ...}) = thm;
 
     val _ = Context.eq_certificate (cert, orig_cert) orelse err "bad theory";
-    val _ = prop aconv orig_prop orelse err "bad prop";
+    val _ = Envir.aeconv (prop, orig_prop) orelse err "bad prop";
     val _ = null constraints orelse err "bad sort constraints";
     val _ = null tpairs orelse err "bad flex-flex constraints";
     val _ = null hyps orelse err "bad hyps";