# HG changeset patch
# User nipkow
# Date 1381952715 -7200
# Node ID 0941a2024569e2ff1c64ce469d5cfaf16ffe0b14
# Parent  c2f18fd05414bd418818063c51807f8598c53538# Parent  4e7d71037bb62a289ae58037ca168cb668e19615
merged

diff -r 4e7d71037bb6 -r 0941a2024569 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Oct 16 21:44:56 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Oct 16 21:45:15 2013 +0200
@@ -971,6 +971,7 @@
               ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE))
               |> the o merge_options;
 
+            val lhs = list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
             val maybe_rhs' = if is_some maybe_rhs then maybe_rhs else
               let
                 fun prove_code_ctr {ctr, sels, ...} =
@@ -990,7 +991,11 @@
               in
                 if exists is_none maybe_ctr_conds_argss then NONE else
                   fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t)
-                    maybe_ctr_conds_argss (Const (@{const_name undefined}, body_type fun_T))
+                    maybe_ctr_conds_argss
+                    (Const (@{const_name Code.abort}, @{typ String.literal} -->
+                        (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
+                      @{term "STR []"} $ (* FIXME *)
+                      absdummy @{typ unit} (incr_boundvars 1 lhs))
                   |> SOME
               end;
           in
@@ -1004,13 +1009,12 @@
                 val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
                 val ms = map (Logic.count_prems o prop_of) ctr_thms;
                 val (raw_t, t) = (raw_rhs, rhs)
-                  |> pairself
-                    (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T),
-                      map Bound (length fun_args - 1 downto 0)))
+                  |> pairself (curry HOLogic.mk_eq lhs
                     #> HOLogic.mk_Trueprop
                     #> curry Logic.list_all (map dest_Free fun_args));
                 val (distincts, discIs, sel_splits, sel_split_asms) =
                   case_thms_of_term lthy bound_Ts raw_rhs;
+val _ = tracing ("code equation: " ^ Syntax.string_of_term lthy t);
 
                 val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
                     sel_split_asms ms ctr_thms