changeset 80712 | 05b16602a683 |
parent 80306 | c2537860ccf8 |
--- a/src/Pure/Tools/simplifier_trace.ML Thu Aug 15 12:22:39 2024 +0200 +++ b/src/Pure/Tools/simplifier_trace.ML Thu Aug 15 12:43:17 2024 +0200 @@ -87,7 +87,7 @@ fun add_thm_breakpoint thm context = let - val rrules = mk_rrules (Context.proof_of context) [thm] + val rrules = mk_rrules (Context.proof_of context) thm in map_breakpoints (apsnd (fold Item_Net.update rrules)) context end