--- a/src/ZF/Zorn.thy Mon Dec 19 13:18:54 1994 +0100
+++ b/src/ZF/Zorn.thy Mon Dec 19 13:24:58 1994 +0100
@@ -11,7 +11,7 @@
Union_in_Pow is proved in ZF.ML
*)
-Zorn = OrderArith + AC + "Inductive" +
+Zorn = OrderArith + AC + Inductive +
consts
Subset_rel :: "i=>i"