diff -r 56034bd1b5f6 -r eb53f944c8cd src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Sun Jun 24 11:41:41 2018 +0100
+++ b/src/ZF/ZF.thy	Sun Jun 24 15:57:48 2018 +0200
@@ -1,6 +1,6 @@
 section\<open>Main ZF Theory: Everything Except AC\<close>
 
-theory ZF imports List_ZF IntDiv_ZF CardinalArith begin
+theory ZF imports List IntDiv CardinalArith begin
 
 (*The theory of "iterates" logically belongs to Nat, but can't go there because
   primrec isn't available into after Datatype.*)