changeset 18358 | 0a733e11021a |
parent 17985 | d5d576b72371 |
child 18377 | 0e1d025d57b3 |
--- a/src/HOLCF/fixrec_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOLCF/fixrec_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -101,7 +101,7 @@ val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint); val fixdefs = map (inferT_axm thy) pre_fixdefs; - val (thy', fixdef_thms) = + val (fixdef_thms, thy') = PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy; val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;