author | lcp |
Thu, 08 Sep 1994 12:55:50 +0200 | |
changeset 591 | 5a6b0ed377cb |
parent 590 | 800603278425 |
child 592 | 9154d8410514 |
--- 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