diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy --- a/src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy Sun Aug 04 13:14:33 2024 +0200 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy Sun Aug 04 13:24:54 2024 +0200 @@ -10,7 +10,7 @@ val compat_plugin = Plugin_Name.declare_setup \<^binding>\compat\; fun compat fp_sugars = - perhaps (try (datatype_compat (map (fst o dest_Type o #T) fp_sugars))); + perhaps (try (datatype_compat (map (dest_Type_name o #T) fp_sugars))); in Theory.setup (fp_sugars_interpretation compat_plugin compat) end