diff -r 817a34a54fb0 -r 946efd210837 src/HOL/MiniML/Maybe.ML
--- a/src/HOL/MiniML/Maybe.ML	Mon May 20 10:11:30 1996 +0200
+++ b/src/HOL/MiniML/Maybe.ML	Mon May 20 18:41:55 1996 +0200
@@ -18,3 +18,7 @@
 by (fast_tac (HOL_cs addss !simpset) 1);
 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";