diff -r 700d4f16b5f2 -r 1c758cd8d5b2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Sun Dec 31 22:04:41 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Sun Dec 31 22:39:40 2023 +0100
@@ -99,7 +99,7 @@
       t' |> map_types
               (map_type_tvar
                 (fn (idxn, sort) =>
-                  if tvar_name_trivial idxn then dummyT else TVar (idxn, sort)))
+                  if tvar_name_trivial idxn then dummyT else raise Same.SAME))
 
     val subst =
       subst |> fold Vartab.delete trivial_tvar_names
@@ -107,7 +107,7 @@
                (K (apsnd (map_type_tfree
                            (fn (name, sort) =>
                               if tfree_name_trivial name then dummyT
-                              else TFree (name, sort)))))
+                              else raise Same.SAME))))
   in
     (t', subst)
   end