tuned;

--- a/src/Pure/Isar/generic_target.ML	Thu Aug 08 16:03:34 2024 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Aug 08 16:21:48 2024 +0200
@@ -122,7 +122,7 @@
 
 fun same_const (Const (c, _), Const (c', _)) = c = c'
   | same_const (t $ _, t' $ _) = same_const (t, t')
-  | same_const (_, _) = false;
+  | same_const _ = false;
 
 fun const_decl phi_pred prmode ((b, mx), rhs) = Morphism.entity (fn phi => fn context =>
   if phi_pred phi then