Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
changeset 79412 1c758cd8d5b2
parent 64429 582f54f6b29b 
--- 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
isabelle