# HG changeset patch
# User wenzelm
# Date 1711979235 -7200
# Node ID 60b6c735b5d5ec01a98e8b6a44ac96439b008392
# Parent  0d94dd2fd2d0b5f3d4473a1349ca0ed23c806696
clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code;

diff -r 0d94dd2fd2d0 -r 60b6c735b5d5 src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Mon Apr 01 15:37:55 2024 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Mon Apr 01 15:47:15 2024 +0200
@@ -372,9 +372,9 @@
 
 fun trace_rrule args ctxt cont =
   let
-    val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args
+    val {unconditional: bool, cterm: cterm, thm: thm, rrule: rrule} = args
     val data =
-      {term = term,
+      {term = Thm.term_of cterm,
        unconditional = unconditional,
        ctxt = ctxt,
        thm = thm,
@@ -395,7 +395,7 @@
 
 val _ = Theory.setup
   (Simplifier.set_trace_ops
-    {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" depth term,
+    {trace_invoke = fn {depth, cterm} => recurse "Simplifier invoked" depth (Thm.term_of cterm),
      trace_rrule = trace_rrule,
      trace_simproc = fn _ => fn ctxt => fn cont => cont ctxt})
 
diff -r 0d94dd2fd2d0 -r 60b6c735b5d5 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Mon Apr 01 15:37:55 2024 +0200
+++ b/src/Pure/raw_simplifier.ML	Mon Apr 01 15:47:15 2024 +0200
@@ -865,8 +865,8 @@
 (* trace operations *)
 
 type trace_ops =
- {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
-  trace_rrule: {unconditional: bool, term: term, thm: thm, rrule: rrule} ->
+ {trace_invoke: {depth: int, cterm: cterm} -> Proof.context -> Proof.context,
+  trace_rrule: {unconditional: bool, cterm: cterm, 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};
@@ -1001,7 +1001,7 @@
         val prop' = Thm.prop_of thm';
         val unconditional = Logic.no_prems prop';
         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
-        val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule};
+        val trace_args = {unconditional = unconditional, cterm = eta_t', thm = thm', rrule = rrule};
       in
         if perm andalso is_greater_equal (term_ord (rhs', lhs'))
         then
@@ -1370,7 +1370,7 @@
       |> Variable.set_body true
       |> Context_Position.set_visible false
       |> inc_simp_depth
-      |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt);
+      |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, cterm = ct} ctxt);
 
     val _ =
       cond_tracing ctxt (fn () =>