Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/export_theory.ML
changeset 70919 692095bafcd9
parent 70917 693e811b91bb
child 70920 1e0ad25c94c8 
--- 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