# HG changeset patch
# User blanchet
# Date 1388652622 -3600
# Node ID 6a6980245ce07892460ce697113156d81b90c14b
# Parent  0ec2cccbf8ad7dbc18aa25aa1afe941463f1f816
robustness

diff -r 0ec2cccbf8ad -r 6a6980245ce0 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- 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);