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 =