diff -r 56034bd1b5f6 -r eb53f944c8cd src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Sun Jun 24 11:41:41 2018 +0100
+++ b/src/ZF/Zorn.thy	Sun Jun 24 15:57:48 2018 +0200
@@ -5,7 +5,7 @@
 
 section\<open>Zorn's Lemma\<close>
 
-theory Zorn imports OrderArith AC Inductive_ZF begin
+theory Zorn imports OrderArith AC Inductive begin
 
 text\<open>Based upon the unpublished article ``Towards the Mechanization of the
 Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.\<close>