allow 'let's around constructors in constructor view

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

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Oct 07 20:54:55 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Oct 07 23:38:57 2013 +0200
@@ -59,6 +59,7 @@
 
   val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     typ list -> term -> term -> term -> term
+  val unfold_let: term -> term
   val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
     typ list -> term -> term
   val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
@@ -283,6 +284,9 @@
     fld [] t o pair []
   end;
 
+fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
+  | unfold_let t = t;
+
 fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
 
 fun massage_let_if_case ctxt has_call massage_leaf =