| changeset 79225 | 2cac47aec8bd |
| parent 79223 | 78d032205af4 |
| child 79227 | a8db9ee24d5e |
--- 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));