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