src/Pure/Thy/export_theory.ML
changeset 70540 04ef5ee3dd4d
parent 70534 fb876ebbf5a7
child 70541 f3fbc7f3559d
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu Aug 15 18:21:12 2019 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Thu Aug 15 19:35:17 2019 +0200
     1.3 @@ -223,8 +223,7 @@
     1.4      fun standard_prop used extra_shyps raw_prop raw_proof =
     1.5        let
     1.6          val raw_proofs = the_list raw_proof;
     1.7 -        val used_proofs = used |> fold Proofterm.used_frees_proof raw_proofs;
     1.8 -        val ([prop], proofs) = ([raw_prop], raw_proofs) |> Proofterm.standard_vars used_proofs;
     1.9 +        val ([prop], proofs) = Proofterm.standard_vars used ([raw_prop], raw_proofs);
    1.10  
    1.11          val args = rev (add_frees used prop []);
    1.12          val typargs = rev (add_tfrees used prop []);