--- a/src/ZF/AC.thy Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/AC.thy Fri Jan 03 15:01:55 1997 +0100
@@ -8,7 +8,7 @@
This definition comes from Halmos (1960), page 59.
*)
-AC = ZF + "func" +
+AC = func +
rules
AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
end