diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/Zorn.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -16,16 +16,19 @@
 *}
 
 definition
-  chain     ::  "'a set set => 'a set set set"
+  chain     ::  "'a set set => 'a set set set" where
   "chain S  = {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
 
-  super     ::  "['a set set,'a set set] => 'a set set set"
+definition
+  super     ::  "['a set set,'a set set] => 'a set set set" where
   "super S c = {d. d \<in> chain S & c \<subset> d}"
 
-  maxchain  ::  "'a set set => 'a set set set"
+definition
+  maxchain  ::  "'a set set => 'a set set set" where
   "maxchain S = {c. c \<in> chain S & super S c = {}}"
 
-  succ      ::  "['a set set,'a set set] => 'a set set"
+definition
+  succ      ::  "['a set set,'a set set] => 'a set set" where
   "succ S c =
     (if c \<notin> chain S | c \<in> maxchain S
     then c else SOME c'. c' \<in> super S c)"