--- a/src/ZF/Univ.thy Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/Univ.thy Fri Jan 03 15:01:55 1997 +0100
@@ -11,7 +11,7 @@
But Ind_Syntax.univ refers to the constant "univ"
*)
-Univ = Arith + Sum + Finite + "mono" +
+Univ = Arith + Sum + Finite + mono +
consts
Vfrom :: [i,i]=>i
Vset :: i=>i