# HG changeset patch
# User panny
# Date 1386010174 -3600
# Node ID ce80d7cd7277c836f1107e19d8517ff8b311ae56
# Parent  985f8b49c050b2092c593b06004c947dc15f5eeb
generate "code" theorems for incomplete definitions

diff -r 985f8b49c050 -r ce80d7cd7277 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Sun Dec 01 19:32:57 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Mon Dec 02 19:49:34 2013 +0100
@@ -1026,20 +1026,21 @@
 
         fun prove_code disc_eqns sel_eqns maybe_exh ctr_alist ctr_specs =
           let
-            val fun_data =
+            val maybe_fun_data =
               (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
                find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns)
               |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x))
               ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE))
               |> merge_options;
           in
-            (case fun_data of
+            (case maybe_fun_data of
               NONE => []
             | SOME (fun_name, fun_T, fun_args, maybe_rhs) =>
               let
                 val bound_Ts = List.rev (map fastype_of fun_args);
 
-                val lhs = list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
+                val lhs =
+                  list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
                 val maybe_rhs_info =
                   (case maybe_rhs of
                     SOME rhs =>
@@ -1067,18 +1068,19 @@
                           end;
                       val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs;
                     in
-                      if exists is_none maybe_ctr_conds_argss then NONE else
-                        let
-                          val rhs = (if exhaustive then
-                              split_last maybe_ctr_conds_argss ||> snd o the
-                            else
-                              Const (@{const_name Code.abort}, @{typ String.literal} -->
-                                  (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
-                                HOLogic.mk_literal fun_name $
-                                absdummy @{typ unit} (incr_boundvars 1 lhs)
-                              |> pair maybe_ctr_conds_argss)
-                            |-> fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t)
-                        in SOME (rhs, rhs, map snd ctr_alist) end
+                      let
+                        val rhs = (if exhaustive
+                              orelse forall is_some maybe_ctr_conds_argss
+                                andalso exists #auto_gen disc_eqns then
+                            split_last (map_filter I maybe_ctr_conds_argss) ||> snd
+                          else
+                            Const (@{const_name Code.abort}, @{typ String.literal} -->
+                                (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
+                              HOLogic.mk_literal fun_name $
+                              absdummy @{typ unit} (incr_boundvars 1 lhs)
+                            |> pair (map_filter I maybe_ctr_conds_argss))
+                          |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u)
+                      in SOME (rhs, rhs, map snd ctr_alist) end
                     end);
               in
                 (case maybe_rhs_info of