src/Pure/Proof/proof_syntax.ML
changeset 71288 06c6495fb1d0
parent 71286 4b45d592ce29
child 71993 3875815f5967
--- 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;