diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Wed Jul 11 11:27:46 2007 +0200
+++ b/src/HOL/Library/Zorn.thy	Wed Jul 11 11:28:13 2007 +0200
@@ -33,12 +33,12 @@
     (if c \<notin> chain S | c \<in> maxchain S
     then c else SOME c'. c' \<in> super S c)"
 
-consts
+inductive_set
   TFin :: "'a set set => 'a set set set"
-inductive "TFin S"
-  intros
+  for S :: "'a set set"
+  where
     succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
-    Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
+  | Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
   monos          Pow_mono