1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Oct 17 10:06:48 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Oct 17 10:29:28 2013 +0200
     1.3 @@ -1003,28 +1003,21 @@
     1.4                let
     1.5                  val rhs = the maybe_rhs';
     1.6                  val bound_Ts = List.rev (map fastype_of fun_args);
     1.7 -                val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs;
     1.8 -                val cond_ctrs =
     1.9 -                  fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs [];
    1.10 -                val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
    1.11 +                val ctr_thms = map snd ctr_alist;
    1.12                  val ms = map (Logic.count_prems o prop_of) ctr_thms;
    1.13 -                val (raw_t, t) = (raw_rhs, rhs)
    1.14 -                  |> pairself (curry HOLogic.mk_eq lhs
    1.15 -                    #> HOLogic.mk_Trueprop
    1.16 -                    #> curry Logic.list_all (map dest_Free fun_args));
    1.17 +                val t = HOLogic.mk_eq (lhs, rhs)
    1.18 +                  |> HOLogic.mk_Trueprop
    1.19 +                  |> curry Logic.list_all (map dest_Free fun_args);
    1.20                  val (distincts, discIs, sel_splits, sel_split_asms) =
    1.21 -                  case_thms_of_term lthy bound_Ts raw_rhs;
    1.22 +                  case_thms_of_term lthy bound_Ts rhs;
    1.23  val _ = tracing ("code equation: " ^ Syntax.string_of_term lthy t);
    1.24  
    1.25 -                val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
    1.26 +                val code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
    1.27                      sel_split_asms ms ctr_thms
    1.28 -                  |> K |> Goal.prove lthy [] [] raw_t;
    1.29 -val _ = tracing ("raw code theorem: " ^ Syntax.string_of_term lthy (prop_of raw_code_thm));
    1.30 +                  |> K |> Goal.prove lthy [] [] t;
    1.31 +val _ = tracing ("code theorem: " ^ Syntax.string_of_term lthy (prop_of code_thm));
    1.32                 in
    1.33 -                 mk_primcorec_code_of_raw_code_tac lthy sel_splits raw_code_thm
    1.34 -                 |> K |> Goal.prove lthy [] [] t
    1.35 -|> tap (tracing o curry (op ^) "code theorem: " o Syntax.string_of_term lthy o prop_of)
    1.36 -                 |> single
    1.37 +                 [code_thm]
    1.38                 end
    1.39  handle ERROR s => (warning s; []) (*###*)
    1.40             end;

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