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));
 
+    val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
+  
   in  thy |> add_defs_i axpairs  end
 
 
 (*external, string-based version; needed?*)
 fun add_fp_def (rec_doms, sintrs) thy =