# HG changeset patch
# User traytel
# Date 1378372251 -7200
# Node ID 01b804df0a3088f7c0ba3bbf1c8901472114e2b3
# Parent  ab4edf89992fb3bb6f61e3ee4d3f99afd05cd2ba
list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors

diff -r ab4edf89992f -r 01b804df0a30 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 05 01:58:48 2013 +0200
+++ b/src/HOL/List.thy	Thu Sep 05 11:10:51 2013 +0200
@@ -548,9 +548,9 @@
         fun check (i, case_t) s =
           (case strip_abs_body case_t of
             (Const (@{const_name List.Nil}, _)) => s
-          | _ => (case s of NONE => SOME i | SOME _ => NONE))
+          | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE))
       in
-        fold_index check cases NONE
+        fold_index check cases (SOME NONE) |> the_default NONE
       end
     (* returns (case_expr type index chosen_case) option  *)
     fun dest_case case_term =