1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 07 20:54:55 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 07 23:38:57 2013 +0200
     1.3 @@ -566,7 +566,7 @@
     1.4      val (lhs, rhs) = HOLogic.dest_eq concl;
     1.5      val fun_name = head_of lhs |> fst o dest_Free;
     1.6      val {ctr_specs, ...} = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name);
     1.7 -    val (ctr, ctr_args) = strip_comb rhs;
     1.8 +    val (ctr, ctr_args) = strip_comb (unfold_let rhs);
     1.9      val {disc, sels, ...} = the (find_first (equal ctr o #ctr) ctr_specs)
    1.10        handle Option.Option => primrec_error_eqn "not a constructor" ctr;
    1.11  
    1.12 @@ -639,7 +639,7 @@
    1.13      else if member (op =) sels head then
    1.14        ([co_dissect_eqn_sel fun_names corec_specs eqn' of_spec concl], matchedsss)
    1.15      else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso
    1.16 -      member (op =) ctrs (head_of (the maybe_rhs)) then
    1.17 +      member (op =) ctrs (head_of (unfold_let (the maybe_rhs))) then
    1.18        co_dissect_eqn_ctr seq fun_names corec_specs eqn' prems concl matchedsss
    1.19      else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso
    1.20        null prems then

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Oct 07 20:54:55 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Oct 07 23:38:57 2013 +0200
     2.3 @@ -59,6 +59,7 @@
     2.4  
     2.5    val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     2.6      typ list -> term -> term -> term -> term
     2.7 +  val unfold_let: term -> term
     2.8    val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
     2.9      typ list -> term -> term
    2.10    val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
    2.11 @@ -283,6 +284,9 @@
    2.12      fld [] t o pair []
    2.13    end;
    2.14  
    2.15 +fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
    2.16 +  | unfold_let t = t;
    2.17 +
    2.18  fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
    2.19  
    2.20  fun massage_let_if_case ctxt has_call massage_leaf =