# HG changeset patch
# User wenzelm
# Date 1723126908 -7200
# Node ID 5dec26c3688d1fd88358f2185d0bab65075c6a1b
# Parent  5aa376b7abb87ae224fd18df515bd47d2f0f368f
tuned;

diff -r 5aa376b7abb8 -r 5dec26c3688d src/Pure/Isar/generic_target.ML
--- 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