changeset 6141 | a6922171b396 |
parent 6112 | 5e4871c5136b |
child 6154 | 6a00a5baef2b |
--- a/src/ZF/Tools/datatype_package.ML Tue Jan 19 11:16:39 1999 +0100 +++ b/src/ZF/Tools/datatype_package.ML Tue Jan 19 11:18:11 1999 +0100 @@ -380,6 +380,7 @@ {big_rec_name = big_rec_name, constructors = constructors, (*let primrec handle definition by cases*) + free_iffs = free_iffs, rec_rewrites = (case recursor_eqns of [] => case_eqns | _ => recursor_eqns)};