# HG changeset patch
# User lcp
# Date 779021750 -7200
# Node ID 5a6b0ed377cbc1aac218fdfa652baef96595ae7e
# Parent  800603278425a22acd9a8d8ec47112ab60b4d100
ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal

diff -r 800603278425 -r 5a6b0ed377cb src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Thu Sep 08 11:05:06 1994 +0200
+++ b/src/ZF/add_ind_def.ML	Thu Sep 08 12:55:50 1994 +0200
@@ -169,6 +169,8 @@
 	     | _ => 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