# HG changeset patch
# User blanchet
# Date 1346794982 -7200
# Node ID 56a50871e25d003981b5d699cdc6afe00b9140a7
# Parent  de13b454fa315586504941dd91d57a8f1f7249a8
smoothly handle one-constructor types

diff -r de13b454fa31 -r 56a50871e25d src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 23:42:33 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 23:43:02 2012 +0200
@@ -189,7 +189,8 @@
       no_defs_lthy
       |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr =>
         fn NONE =>
-           if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl)
+           if n = 1 then pair (Term.lambda v @{term True}, refl)
+           else if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl)
            else pair (not_other_disc k, missing_disc_def)
          | SOME b => Specification.definition (SOME (b, NONE, NoSyn),
              ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd)