src/ZF/Constructible/Datatype_absolute.thy

 lemma (in M_axioms) list_functor_abs [simp]: 
      "[| M(A); M(X); M(Z) |] ==> is_list_functor(M,A,X,Z) <-> (Z = {0} + A*X)"
 by (simp add: is_list_functor_def singleton_0 nat_into_M)
 
 
-locale M_datatypes = M_wfrank +
+locale (open) M_datatypes = M_wfrank +
  assumes list_replacement1: 
    "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
   and list_replacement2: 
    "M(A) ==> strong_replacement(M, 
          \<lambda>n y. n\<in>nat &