--- a/src/ZF/Inductive.thy Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Inductive.thy Mon Dec 28 16:59:28 1998 +0100
@@ -1,5 +1,5 @@
(*Dummy theory to document dependencies *)
-Inductive = Fixedpt + Sum + QPair + "indrule" +
+Inductive = Fixedpt + Sum + QPair +
end