diff -r 978ee7ededdd -r f7a573c46611 src/HOL/MiniML/Maybe.ML
--- a/src/HOL/MiniML/Maybe.ML	Wed May 22 16:54:16 1996 +0200
+++ b/src/HOL/MiniML/Maybe.ML	Wed May 22 17:11:54 1996 +0200
@@ -19,6 +19,10 @@
 by (Asm_simp_tac 1);
 qed "expand_bind";
 
-goal Maybe.thy "!!x. x = Ok y ==> x ~= Fail";
-by(Asm_simp_tac 1);
-qed "eq_OkD";
+goal Maybe.thy
+  "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
+by(simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by(fast_tac HOL_cs 1);
+qed "bind_eq_Fail";
+
+Addsimps [bind_eq_Fail];