
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>\<open>compat\<close>;
 
   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




