src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
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