src/ZF/Tools/datatype_package.ML
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)};