# HG changeset patch
# User wenzelm
# Date 1571603204 -7200
# Node ID 692095bafcd905513fc439e66a4690f1f4463805
# Parent  d36f600c6500c63448228ba12ac3f2c77f047887
avoid spurious shyps (with vacous type variable);

diff -r d36f600c6500 -r 692095bafcd9 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sun Oct 20 21:42:13 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sun Oct 20 22:26:44 2019 +0200
@@ -278,7 +278,7 @@
     fun encode_thm thm_id raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
-        val thm = Thm.unconstrainT (clean_thm raw_thm);
+        val thm = clean_thm (Thm.unconstrainT raw_thm);
         val boxes = proof_boxes_of thm thm_id;
 
         val proof0 =