changeset 50295 | 52413dc96326 |
parent 50293 | 718e4ad1517e |
child 50301 | dde4967c9233 |
1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 16:08:27 2012 +0200 1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 16:08:55 2012 +0200 1.3 @@ -480,7 +480,7 @@ 1.4 corec_def), lthy) 1.5 end; 1.6 in 1.7 - wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, sel_binderss)) lthy' 1.8 + wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss, []))) lthy' 1.9 |> (if lfp then some_lfp_sugar else some_gfp_sugar) 1.10 end; 1.11