diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Inductive.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -1,3 +1,4 @@
-Inductive = Gfp + Prod + Sum + "indrule"
+Inductive = Gfp + Prod + Sum +
 
+end