src/ZF/add_ind_def.ML

 	   (case parts of 
 	       [_] => [] 			(*no mutual recursion*)
 	     | _ => rec_tms ~~		(*define the sets as Parts*)
 		    map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
 
-  in  thy |> add_defns_i axpairs  end
+  in  thy |> add_defs_i axpairs  end
 
 
 (*external, string-based version; needed?*)
 fun add_fp_def (rec_doms, sintrs) thy = 
   let val sign = sign_of thy;

 	(big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
 
     val axpairs =
 	big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))
 
-    in  thy |> add_consts_i const_decs |> add_defns_i axpairs  end;
+    in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
 end;
-
-
-
-