1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Sun Dec 01 19:32:57 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Mon Dec 02 19:49:34 2013 +0100
     1.3 @@ -1026,20 +1026,21 @@
     1.4  
     1.5          fun prove_code disc_eqns sel_eqns maybe_exh ctr_alist ctr_specs =
     1.6            let
     1.7 -            val fun_data =
     1.8 +            val maybe_fun_data =
     1.9                (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
    1.10                 find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns)
    1.11                |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x))
    1.12                ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE))
    1.13                |> merge_options;
    1.14            in
    1.15 -            (case fun_data of
    1.16 +            (case maybe_fun_data of
    1.17                NONE => []
    1.18              | SOME (fun_name, fun_T, fun_args, maybe_rhs) =>
    1.19                let
    1.20                  val bound_Ts = List.rev (map fastype_of fun_args);
    1.21  
    1.22 -                val lhs = list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
    1.23 +                val lhs =
    1.24 +                  list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
    1.25                  val maybe_rhs_info =
    1.26                    (case maybe_rhs of
    1.27                      SOME rhs =>
    1.28 @@ -1067,18 +1068,19 @@
    1.29                            end;
    1.30                        val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs;
    1.31                      in
    1.32 -                      if exists is_none maybe_ctr_conds_argss then NONE else
    1.33 -                        let
    1.34 -                          val rhs = (if exhaustive then
    1.35 -                              split_last maybe_ctr_conds_argss ||> snd o the
    1.36 -                            else
    1.37 -                              Const (@{const_name Code.abort}, @{typ String.literal} -->
    1.38 -                                  (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
    1.39 -                                HOLogic.mk_literal fun_name $
    1.40 -                                absdummy @{typ unit} (incr_boundvars 1 lhs)
    1.41 -                              |> pair maybe_ctr_conds_argss)
    1.42 -                            |-> fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t)
    1.43 -                        in SOME (rhs, rhs, map snd ctr_alist) end
    1.44 +                      let
    1.45 +                        val rhs = (if exhaustive
    1.46 +                              orelse forall is_some maybe_ctr_conds_argss
    1.47 +                                andalso exists #auto_gen disc_eqns then
    1.48 +                            split_last (map_filter I maybe_ctr_conds_argss) ||> snd
    1.49 +                          else
    1.50 +                            Const (@{const_name Code.abort}, @{typ String.literal} -->
    1.51 +                                (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
    1.52 +                              HOLogic.mk_literal fun_name $
    1.53 +                              absdummy @{typ unit} (incr_boundvars 1 lhs)
    1.54 +                            |> pair (map_filter I maybe_ctr_conds_argss))
    1.55 +                          |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u)
    1.56 +                      in SOME (rhs, rhs, map snd ctr_alist) end
    1.57                      end);
    1.58                in
    1.59                  (case maybe_rhs_info of