diff -r 41f3ca717da5 -r c71a44893645 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Jan 07 12:37:12 2020 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Jan 07 14:58:01 2020 +0100
@@ -3022,12 +3022,7 @@
 
     lift_bnf 'a myoption (*<*)[wits: "Inl undefined :: 'a + 'a"](*>*)
 
-    proof (intro rel_funI)
-      fix f g :: "'a \<Rightarrow> 'b" and x y :: "'a + 'a"
-      assume "f = g" "ignore_Inl x y"
-      then show "ignore_Inl (map_sum f f x) (map_sum g g y)"
-        by (cases x; cases y) auto
-    next
+    proof -
       fix P :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and Q :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
       assume "P OO Q \<noteq> bot"
       then show "rel_sum P P OO ignore_Inl OO rel_sum Q Q