# HG changeset patch
# User nipkow
# Date 1709049979 -3600
# Node ID 8ae4fc4692e8b2003ec95890ffdd2d6589b71080
# Parent  9c00a46d69d09634e802e7726de4214198e979aa
tuned name

diff -r 9c00a46d69d0 -r 8ae4fc4692e8 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Feb 27 11:59:47 2024 +0100
+++ b/src/Pure/raw_simplifier.ML	Tue Feb 27 17:06:19 2024 +0100
@@ -868,7 +868,7 @@
  {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
   trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} ->
     Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option,
-  trace_simproc: {name: string, goal: cterm} ->
+  trace_simproc: {name: string, cterm: cterm} ->
     Proof.context -> (Proof.context -> thm option) -> thm option};
 
 structure Trace_Ops = Theory_Data
@@ -1063,7 +1063,7 @@
               print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
              (let
                 val ctxt' = Config.put simp_trace (Config.get ctxt simp_debug) ctxt
-                val res = trace_simproc {name = name, goal = eta_t'} ctxt'
+                val res = trace_simproc {name = name, cterm = eta_t'} ctxt'
                   (fn ctxt'' => Morphism.form_context' ctxt'' proc eta_t')
               in case res of
                 NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps)