src/HOL/Library/Nested_Environment.thy

   shows "\<exists>e. lookup env xs = Some e"
 proof -
   from prems have "lookup env (xs @ ys) \<noteq> None" by simp
   then have "lookup env xs \<noteq> None"
     by (rule contrapos_nn) (simp only: lookup_append_none)
-  then show ?thesis by (simp add: not_None_eq)
+  then show ?thesis by (simp)
 qed
 
 text {*
   The subsequent statement describes in more detail how a successful
   @{term lookup} with a non-empty path results in a certain situation