--- a/src/HOL/Nominal/Examples/Class1.thy Sun Aug 01 23:18:13 2021 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy Mon Aug 02 10:01:06 2021 +0000
@@ -8,6 +8,8 @@
text \<open>types\<close>
+no_notation not ("NOT")
+
nominal_datatype ty =
PR "string"
| NOT "ty"