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/choice_specification.ML
changeset 79412 1c758cd8d5b2
parent 79336 032a31db4c6f
child 80636 4041e7c8059d 
--- a/src/HOL/Tools/choice_specification.ML	Sun Dec 31 22:04:41 2023 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Sun Dec 31 22:39:40 2023 +0100
@@ -60,7 +60,7 @@
     val fmap' = map Library.swap fmap
     fun unthaw v =
       (case AList.lookup (op =) fmap' v of
-        NONE => TVar v
+        NONE => raise Same.SAME
       | SOME w => TFree w)
   in map_types (map_type_tvar unthaw) t end
isabelle