diff -r 4dc65845eab3 -r d8d7d1b785af doc-src/ZF/ZF_examples.thy
--- a/doc-src/ZF/ZF_examples.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/doc-src/ZF/ZF_examples.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -64,7 +64,7 @@
      "t \<in> bt(A) ==> \<forall>k \<in> nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
   by (induct_tac t, simp_all) 
 
-constdefs  n_nodes_tail :: "i => i"
+definition n_nodes_tail :: "i => i" where
    "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
 
 lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"