diff -r e74f694ca1da -r c7a8f374339b src/HOL/MiniML/Maybe.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MiniML/Maybe.thy	Wed Oct 25 09:46:46 1995 +0100
@@ -0,0 +1,18 @@
+(* Title:     HOL/MiniML/Maybe.thy
+   ID:        $Id$
+   Author:    Dieter Nazareth and Tobias Nipkow
+   Copyright  1995 TU Muenchen
+
+Universal error monad.
+*)
+
+Maybe = List +
+
+datatype 'a maybe =  Ok 'a | Fail
+
+consts bind :: "['a maybe, 'a => 'b maybe] => 'b maybe" (infixl 60)
+
+defs
+  bind_def "m bind f == case m of Ok r => f r | Fail => Fail"
+
+end