From 3467e685b624580a5737f062cc90b949a4fbef98 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Wed, 1 Feb 2023 18:21:08 +1100
Subject: [PATCH] lib: remove opt_mapE from global [elim!] set

While we do want to break up full OptionMonad terms in assumptions, we
do not usually want to break up projections.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 lib/Monads/OptionMonad.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Monads/OptionMonad.thy b/lib/Monads/OptionMonad.thy
index 713431add..79543639b 100644
--- a/lib/Monads/OptionMonad.thy
+++ b/lib/Monads/OptionMonad.thy
@@ -416,7 +416,7 @@ lemma oreturnOkE:
   by simp
 
 lemmas omonadE [elim!] =
-  opt_mapE obindE oreturnE ofailE othrowE oreturnOkE oassertE
+  obindE oreturnE ofailE othrowE oreturnOkE oassertE
 
 lemma in_opt_map_Some_eq:
   "((f ||> g) x = Some y) = (\<exists>v. f x = Some v \<and> g v = y)"