# 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 =