# HG changeset patch
# User wenzelm
# Date 951404665 -3600
# Node ID c721220203803b7674072d2c3ef959157f5c78a5
# Parent  ed9fc488b9801a27d26a0a9f8416c5abc8b446cb
tuned;

diff -r ed9fc488b980 -r c72122020380 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Feb 24 16:01:34 2000 +0100
+++ b/src/Pure/thm.ML	Thu Feb 24 16:04:25 2000 +0100
@@ -646,13 +646,12 @@
   If this check must be made, recalculate maxidx in hope of preventing its
   recurrence.*)
 fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s =
-  (Sign.nodup_vars prop; 
-   Thm {sign_ref = sign_ref, 
+  Thm {sign_ref = sign_ref, 
          der = der,     
          maxidx = maxidx_of_term prop,
          shyps = shyps, 
          hyps = hyps, 
-         prop = prop})
+         prop = Sign.nodup_vars prop}
   handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts);