retain type information from reconstruct_proof, notably for Export_Theory.export_thm;

--- 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;