# HG changeset patch
# User wenzelm
# Date 1573240377 -3600
# Node ID 06c6495fb1d08c63e9dfa6622f95432163d71e8e
# Parent  907b7a6471a0d4125129dad40627bc1a09cc1f3f
retain type information from reconstruct_proof, notably for Export_Theory.export_thm;

diff -r 907b7a6471a0 -r 06c6495fb1d0 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Nov 08 20:12:06 2019 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Nov 08 20:12:57 2019 +0100
@@ -286,7 +286,7 @@
   let val thy = Thm.theory_of_thm thm in
     Thm.reconstruct_proof_of thm
     |> Proofterm.expand_proof thy expand_name
-    |> Proofterm.rew_proof thy
+    |> Proofterm.rewrite_proof thy ([], Proof_Rewrite_Rules.rprocs true)
     |> Proofterm.no_thm_proofs
     |> not full ? Proofterm.shrink_proof
   end;