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 70605 048cf2096186
parent 70604 8088cf2576f3
child 70784 799437173553 
--- a/src/Pure/Thy/export_theory.ML	Fri Aug 23 13:32:27 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Aug 23 14:32:51 2019 +0200
@@ -259,7 +259,7 @@
 
     fun encode_thm raw_thm =
       let
-        val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy raw_thm);
+        val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
         val thm = clean_thm raw_thm;
         val raw_proof =
           if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else Proofterm.MinProof;
isabelle