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 =