# HG changeset patch
# User wenzelm
# Date 1711978675 -7200
# Node ID 0d94dd2fd2d0b5f3d4473a1349ca0ed23c806696
# Parent  588ea80f16bbedabb1c7231f885b0d029ac21cf5
clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);
NB: Simplifier.set_trace_ops overrides Pure setup for Simplifier_Trace panel, but that is hardly every used in practice;

diff -r 588ea80f16bb -r 0d94dd2fd2d0 src/Pure/Tools/simplifier_trace.ML
--- 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 _ =
diff -r 588ea80f16bb -r 0d94dd2fd2d0 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Mon Apr 01 15:09:30 2024 +0200
+++ b/src/Pure/raw_simplifier.ML	Mon Apr 01 15:37:55 2024 +0200
@@ -866,7 +866,7 @@
 
 type trace_ops =
  {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
-  trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} ->
+  trace_rrule: {unconditional: bool, term: term, thm: thm, rrule: rrule} ->
     Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option,
   trace_simproc: {name: string, cterm: cterm} ->
     Proof.context -> (Proof.context -> thm option) -> thm option};
@@ -876,7 +876,7 @@
   type T = trace_ops;
   val empty: T =
    {trace_invoke = fn _ => fn ctxt => ctxt,
-    trace_apply = fn _ => fn ctxt => fn cont => cont ctxt,
+    trace_rrule = fn _ => fn ctxt => fn cont => cont ctxt,
     trace_simproc = fn _ => fn ctxt => fn cont => cont ctxt};
   fun merge (trace_ops, _) = trace_ops;
 );
@@ -885,7 +885,7 @@
 
 val trace_ops = Trace_Ops.get o Proof_Context.theory_of;
 fun trace_invoke args ctxt = #trace_invoke (trace_ops ctxt) args ctxt;
-fun trace_apply args ctxt = #trace_apply (trace_ops ctxt) args ctxt;
+fun trace_rrule args ctxt = #trace_rrule (trace_ops ctxt) args ctxt;
 fun trace_simproc args ctxt = #trace_simproc (trace_ops ctxt) args ctxt;
 
 
@@ -1015,7 +1015,7 @@
           if unconditional
           then
            (cond_tracing ctxt (fn () => print_thm ctxt "Rewriting:" ("", thm'));
-            trace_apply trace_args ctxt (fn ctxt' =>
+            trace_rrule trace_args ctxt (fn ctxt' =>
               let
                 val lr = Logic.dest_equals prop;
                 val SOME thm'' = check_conv ctxt' false eta_thm thm';
@@ -1025,7 +1025,7 @@
             if simp_depth ctxt > Config.get ctxt simp_depth_limit
             then (cond_tracing ctxt (fn () => "simp_depth_limit exceeded - giving up"); NONE)
             else
-              trace_apply trace_args ctxt (fn ctxt' =>
+              trace_rrule trace_args ctxt (fn ctxt' =>
                 (case prover ctxt' thm' of
                   NONE => (cond_tracing ctxt' (fn () => print_thm ctxt' "FAILED" ("", thm')); NONE)
                 | SOME thm2 =>