graceful handling of abort

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Oct 17 10:06:48 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Oct 17 10:29:28 2013 +0200
@@ -1003,28 +1003,21 @@
               let
                 val rhs = the maybe_rhs';
                 val bound_Ts = List.rev (map fastype_of fun_args);
-                val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs;
-                val cond_ctrs =
-                  fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs [];
-                val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
+                val ctr_thms = map snd ctr_alist;
                 val ms = map (Logic.count_prems o prop_of) ctr_thms;
-                val (raw_t, t) = (raw_rhs, rhs)
-                  |> pairself (curry HOLogic.mk_eq lhs
-                    #> HOLogic.mk_Trueprop
-                    #> curry Logic.list_all (map dest_Free fun_args));
+                val t = HOLogic.mk_eq (lhs, rhs)
+                  |> 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;
+                  case_thms_of_term lthy bound_Ts 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
+                val code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
                     sel_split_asms ms ctr_thms
-                  |> K |> Goal.prove lthy [] [] raw_t;
-val _ = tracing ("raw code theorem: " ^ Syntax.string_of_term lthy (prop_of raw_code_thm));
+                  |> K |> Goal.prove lthy [] [] t;
+val _ = tracing ("code theorem: " ^ Syntax.string_of_term lthy (prop_of code_thm));
                in
-                 mk_primcorec_code_of_raw_code_tac lthy sel_splits raw_code_thm
-                 |> K |> Goal.prove lthy [] [] t
-|> tap (tracing o curry (op ^) "code theorem: " o Syntax.string_of_term lthy o prop_of)
-                 |> single
+                 [code_thm]
                end
 handle ERROR s => (warning s; []) (*###*)
            end;

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Oct 17 10:06:48 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Oct 17 10:29:28 2013 +0200
@@ -103,9 +103,11 @@
      eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
      (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))));
 
-fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms ctr_thms =
-  EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
-    ms ctr_thms);
+fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs =
+  EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) ms
+    f_ctrs) THEN
+  IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
+    HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)));
 
 fun mk_primcorec_code_of_raw_code_tac ctxt splits raw =
   HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'