Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid spurious shyps (with vacous type variable);
authorwenzelm
Sun, 20 Oct 2019 22:26:44 +0200
changeset 70919 692095bafcd9
parent 70918 d36f600c6500
child 70920 1e0ad25c94c8
avoid spurious shyps (with vacous type variable);
src/Pure/Thy/export_theory.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle