src/ZF/Constructible/Rec_Separation.thy

   apply (rule M_trancl_axioms.intro)
    apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+
   done
 
 theorem M_trancl_L: "PROP M_trancl(L)"
-by (rule M_trancl.intro
-         [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L])
-
-interpretation M_trancl [L] by (rule M_trancl_axioms_L)
+by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
+
+interpretation M_trancl [L] by (rule M_trancl_L)
 
 
 subsection{*@{term L} is Closed Under the Operator @{term list}*}
 
 subsubsection{*Instances of Replacement for Lists*}

         nth_replacement)+
   done
 
 theorem M_datatypes_L: "PROP M_datatypes(L)"
   apply (rule M_datatypes.intro)
-      apply (rule M_trancl.axioms [OF M_trancl_L])+
- apply (rule M_datatypes_axioms_L) 
- done
-
-interpretation M_datatypes [L] by (rule M_datatypes_axioms_L)
+   apply (rule M_trancl_L)
+  apply (rule M_datatypes_axioms_L) 
+  done
+
+interpretation M_datatypes [L] by (rule M_datatypes_L)
 
 
 subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
 
 subsubsection{*Instances of Replacement for @{term eclose}*}

    apply (assumption | rule eclose_replacement1 eclose_replacement2)+
   done
 
 theorem M_eclose_L: "PROP M_eclose(L)"
   apply (rule M_eclose.intro)
-       apply (rule M_datatypes.axioms [OF M_datatypes_L])+
+   apply (rule M_datatypes_L)
   apply (rule M_eclose_axioms_L)
   done
 
-interpretation M_eclose [L] by (rule M_eclose_axioms_L)
+interpretation M_eclose [L] by (rule M_eclose_L)
 
 
 end