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/Types_To_Sets/internalize_sort.ML
changeset 77869 1156aa9db7f5
parent 77730 4a174bea55e2
child 79390 a20e6cdc729a 
--- a/src/HOL/Types_To_Sets/internalize_sort.ML	Tue Apr 18 12:10:00 2023 +0200
+++ b/src/HOL/Types_To_Sets/internalize_sort.ML	Tue Apr 18 12:23:37 2023 +0200
@@ -31,7 +31,7 @@
     val thy = Thm.theory_of_thm thm;
     val tvar = Thm.typ_of ctvar;
 
-    val (ucontext, _) = Logic.unconstrainT Sortset.empty (Thm.prop_of thm);
+    val (ucontext, _) = Logic.unconstrainT [] (Thm.prop_of thm);
 
     fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
     fun reduce_to_non_proper_sort (TVar (name, sort)) =
isabelle