# HG changeset patch
# User haftmann
# Date 1755019001 -7200
# Node ID af4cad931c51ad91ceb85e688ec19263cc6a225c
# Parent  9dc2e315525785de6f85d945380e34b39b23f424
tuned name

diff -r 9dc2e3155257 -r af4cad931c51 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Aug 12 12:30:31 2025 +0200
+++ b/src/Pure/Isar/class.ML	Tue Aug 12 19:16:41 2025 +0200
@@ -362,12 +362,12 @@
     val rhs2 = Morphism.term phi2 rhs;
   in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end;
 
-fun target_const class phi0 prmode (b, rhs) lthy =
+fun target_const class phi prmode (b, rhs) lthy =
   let
     val export =
       Morphism.set_context' lthy (Variable.export_morphism lthy (Local_Theory.target_of lthy));
     val guess_identity = guess_morphism_identity (b, rhs) export;
-    val guess_canonical = guess_morphism_identity (b, rhs) (export $> phi0);
+    val guess_canonical = guess_morphism_identity (b, rhs) (export $> phi);
   in
     lthy
     |> Generic_Target.locale_target_const class