# HG changeset patch
# User wenzelm
# Date 1702154930 -3600
# Node ID 2cac47aec8bd688ab5dbf70fd53fa432da523e01
# Parent  936ad4627a74c308bf915603339bc01b8efa8d07
avoid accidental capture of theory value, and thus reduce heap size again (amending 5109e4b2a292);

diff -r 936ad4627a74 -r 2cac47aec8bd src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Dec 09 21:25:26 2023 +0100
+++ b/src/Pure/proofterm.ML	Sat Dec 09 21:48:50 2023 +0100
@@ -1593,7 +1593,7 @@
   let val (rules, procs) = #1 (Data.get thy)
   in (map #2 rules, map #2 procs) end;
 
-fun rew_proof thy prf = rewrite_prf fst (get_rew_data thy) prf;
+fun rew_proof thy = rewrite_prf fst (get_rew_data thy);
 
 fun add_prf_rrule r = (Data.map o apfst o apfst) (cons (stamp (), r));
 fun add_prf_rproc p = (Data.map o apfst o apsnd) (cons (stamp (), p));