diff -r 96f51689cdeb -r 6330ca0a3ac5 src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Mon Dec 19 13:18:54 1994 +0100
+++ b/src/ZF/Finite.thy	Mon Dec 19 13:24:58 1994 +0100
@@ -6,7 +6,7 @@
 Finite powerset operator
 *)
 
-Finite = Arith + "Inductive" +
+Finite = Arith + Inductive +
 consts
   Fin 	    :: "i=>i"
   FiniteFun :: "[i,i]=>i"		("(_ -||>/ _)" [61, 60] 60)