--- a/src/HOL/MiniML/Maybe.thy Wed Mar 06 14:12:24 1996 +0100
+++ b/src/HOL/MiniML/Maybe.thy Wed Mar 06 14:19:39 1996 +0100
@@ -10,10 +10,9 @@
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"
+constdefs
+ bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
+ "m bind f == case m of Ok r => f r | Fail => Fail"
syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
translations "P := E; F" == "E bind (%P.F)"