src/HOL/Tools/Nunchaku/nunchaku_collect.ML

--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Mon Jan 08 21:54:20 2024 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Mon Jan 08 22:26:04 2024 +0100
@@ -190,7 +190,7 @@
       raise UNEXPECTED_POLYMORPHISM t
     else
       t
-      |> attach_typeS
+      |> Term.smash_sorts \<^sort>\<open>type\<close>
       |> whack_term thy whacks
       |> Object_Logic.atomize_term ctxt
       |> tap (fn t' => fastype_of t' <> \<^typ>\<open>prop\<close> orelse raise TOO_META t)