list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
authortraytel
Thu Sep 05 11:10:51 2013 +0200 (2013-09-05)
changeset 5341201b804df0a30
parent 53411 ab4edf89992f
child 53413 ca3fdc640ebf
list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Thu Sep 05 01:58:48 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Sep 05 11:10:51 2013 +0200
     1.3 @@ -548,9 +548,9 @@
     1.4          fun check (i, case_t) s =
     1.5            (case strip_abs_body case_t of
     1.6              (Const (@{const_name List.Nil}, _)) => s
     1.7 -          | _ => (case s of NONE => SOME i | SOME _ => NONE))
     1.8 +          | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE))
     1.9        in
    1.10 -        fold_index check cases NONE
    1.11 +        fold_index check cases (SOME NONE) |> the_default NONE
    1.12        end
    1.13      (* returns (case_expr type index chosen_case) option  *)
    1.14      fun dest_case case_term =