diff -r 6928771d256e -r ea88ddeafabe src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Sep 29 00:58:54 2005 +0200
+++ b/src/HOL/Set.thy	Thu Sep 29 00:58:55 2005 +0200
@@ -305,6 +305,9 @@
 axioms
   mem_Collect_eq: "(a : {x. P(x)}) = P(a)"
   Collect_mem_eq: "{x. x:A} = A"
+finalconsts
+  Collect
+  "op :"
 
 defs
   Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"