# HG changeset patch
# User wenzelm
# Date 1187385045 -7200
# Node ID 5a6342236a32a3c853f4133ff3563d697df7536b
# Parent  bb5ec06f7c7a2d8185ab10ccc653bb7745c404fb
compress: proper check_thy;

diff -r bb5ec06f7c7a -r 5a6342236a32 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 17 23:10:43 2007 +0200
+++ b/src/Pure/thm.ML	Fri Aug 17 23:10:45 2007 +0200
@@ -581,15 +581,20 @@
 (*Compression of theorems -- a separate rule, not integrated with the others,
   as it could be slow.*)
 fun compress (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
-  let val thy = Theory.deref thy_ref in
-    Thm {thy_ref = thy_ref,
+  let
+    val thy = Theory.deref thy_ref;
+    val hyps' = map (Compress.term thy) hyps;
+    val tpairs' = map (pairself (Compress.term thy)) tpairs;
+    val prop' = Compress.term thy prop;
+  in
+    Thm {thy_ref = Theory.check_thy thy,
       der = der,
       tags = tags,
       maxidx = maxidx,
       shyps = shyps,
-      hyps = map (Compress.term thy) hyps,
-      tpairs = map (pairself (Compress.term thy)) tpairs,
-      prop = Compress.term thy prop}
+      hyps = hyps',
+      tpairs = tpairs',
+      prop = prop'}
   end;
 
 fun norm_proof (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =