diff -r 345e592792fd -r c84c0c0e6907 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 11:01:44 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 11:05:36 2025 +0100
@@ -219,7 +219,7 @@
     val th2 = meta_mp nonempty td_th
     val c =
       case Thm.concl_of th2 of
-        _ $ (Const(\<^const_name>\<open>Ex\<close>,_) $ Abs(_,_,Const(\<^const_name>\<open>Set.member\<close>,_) $ _ $ c)) => c
+        \<^Const_>\<open>Trueprop for \<^Const_>\<open>Ex _ for \<open>Abs (_, _, \<^Const_>\<open>Set.member _ for _ c\<close>)\<close>\<close>\<close> => c
       | _ => error "type_introduction: bad type definition theorem"
     val tfrees = Term.add_tfrees c []
     val tnames = sort_strings (map fst tfrees)