more finalconsts;

--- a/src/FOL/IFOL.thy	Thu Sep 29 00:58:54 2005 +0200
+++ b/src/FOL/IFOL.thy	Thu Sep 29 00:58:55 2005 +0200
@@ -16,6 +16,7 @@
 global
 
 classes "term"
+final_consts term_class
 defaultsort "term"
 
 typedecl o

--- a/src/HOL/Hilbert_Choice.thy	Thu Sep 29 00:58:54 2005 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 29 00:58:55 2005 +0200
@@ -34,6 +34,8 @@
 
 axioms
   someI: "P (x::'a) ==> P (SOME x. P x)"
+finalconsts
+  Eps
 
 
 constdefs

--- a/src/HOL/Nat.thy	Thu Sep 29 00:58:54 2005 +0200
+++ b/src/HOL/Nat.thy	Thu Sep 29 00:58:55 2005 +0200
@@ -24,7 +24,9 @@
   -- {* the axiom of infinity in 2 parts *}
   inj_Suc_Rep:          "inj Suc_Rep"
   Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
-
+finalconsts
+  Zero_Rep
+  Suc_Rep
 
 subsection {* Type nat *}
 

--- 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)"