author | blanchet |
Thu, 02 Jan 2014 09:50:22 +0100 | |
changeset 54911 | 6a6980245ce0 |
parent 54910 | 0ec2cccbf8ad |
child 54912 | 4ecdea61181e |
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100 @@ -348,6 +348,7 @@ fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels}; in map3 mk_spec ctrs discs selss + handle ListPair.UnequalLengths => not_codatatype ctxt res_T end) | _ => not_codatatype ctxt res_T);