--- a/src/ZF/Induct/Datatypes.thy Tue Sep 27 17:03:23 2022 +0100
+++ b/src/ZF/Induct/Datatypes.thy Tue Sep 27 17:46:52 2022 +0100
@@ -14,7 +14,7 @@
\<close>
consts
- data :: "[i, i] => i"
+ data :: "[i, i] \<Rightarrow> i"
datatype "data(A, B)" =
Con0