src/Pure/Thy/export_theory.ML

--- a/src/Pure/Thy/export_theory.ML	Thu Aug 15 18:21:12 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Thu Aug 15 19:35:17 2019 +0200
@@ -223,8 +223,7 @@
     fun standard_prop used extra_shyps raw_prop raw_proof =
       let
         val raw_proofs = the_list raw_proof;
-        val used_proofs = used |> fold Proofterm.used_frees_proof raw_proofs;
-        val ([prop], proofs) = ([raw_prop], raw_proofs) |> Proofterm.standard_vars used_proofs;
+        val ([prop], proofs) = Proofterm.standard_vars used ([raw_prop], raw_proofs);
 
         val args = rev (add_frees used prop []);
         val typargs = rev (add_tfrees used prop []);