--- a/src/Pure/Tools/simplifier_trace.ML Mon Apr 01 15:09:30 2024 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML Mon Apr 01 15:37:55 2024 +0200
@@ -370,7 +370,7 @@
(** setup **)
-fun simp_apply args ctxt cont =
+fun trace_rrule args ctxt cont =
let
val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args
val data =
@@ -387,7 +387,7 @@
(case res of
NONE =>
if Future.join (indicate_failure data ctxt') then
- simp_apply args ctxt cont
+ trace_rrule args ctxt cont
else NONE
| SOME (thm, _) => (indicate_success thm ctxt'; res))
end)
@@ -396,7 +396,7 @@
val _ = Theory.setup
(Simplifier.set_trace_ops
{trace_invoke = fn {depth, term} => recurse "Simplifier invoked" depth term,
- trace_apply = simp_apply,
+ trace_rrule = trace_rrule,
trace_simproc = fn _ => fn ctxt => fn cont => cont ctxt})
val _ =