Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned name
authorhaftmann
Tue, 12 Aug 2025 19:16:41 +0200
changeset 83000 af4cad931c51
parent 82999 9dc2e3155257
child 83001 157aaea4c42c
tuned name
src/Pure/Isar/class.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle