src/ZF/Constructible/WFrec.thy

--- a/src/ZF/Constructible/WFrec.thy	Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/WFrec.thy	Tue Nov 07 19:40:13 2006 +0100
@@ -271,7 +271,7 @@
 
 subsection{*Relativization of the ZF Predicate @{term is_recfun}*}
 
-constdefs
+definition
   M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    "M_is_recfun(M,MH,r,a,f) == 
      \<forall>z[M]. z \<in> f <->