simplified code

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 20:29:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 21:25:53 2013 +0200
@@ -579,7 +579,8 @@
       val {fun_args, rhs_term, ... } = the maybe_sel_eqn;
       fun rewrite_q _ t = if has_call t then @{term False} else @{term True};
       fun rewrite_g _ t = if has_call t then undef_const else t;
-      fun rewrite_h _ t = if has_call t then HOLogic.mk_tuple (snd (strip_comb t)) else undef_const;
+      fun rewrite_h bound_Ts t =
+        if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const;
       fun massage f t = massage_direct_corec_call lthy has_call f [] rhs_term |> abs_tuple fun_args;
     in
       (massage rewrite_q,
@@ -591,23 +592,28 @@
 fun build_corec_arg_indirect_call lthy has_call sel_eqns sel =
   let
     val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
-    fun rewrite bound_Ts U T (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) U T b)
-      | rewrite bound_Ts U T (t as _ $ _) =
-        let val (u, vs) = strip_comb t in
-          if is_Free u andalso has_call u then
-            Inr_const U T $ mk_tuple1 bound_Ts vs
-          else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
-            list_comb (map_types (K dummyT) u, map (rewrite bound_Ts U T) vs)
-          else
-            list_comb (rewrite bound_Ts U T u, map (rewrite bound_Ts U T) vs)
-        end
-      | rewrite _ U T t = if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t;
-    fun massage NONE t = t
-      | massage (SOME {fun_args, rhs_term, ...}) t =
+  in
+    if is_none maybe_sel_eqn then I else
+    let
+      val {fun_args, rhs_term, ...} = the maybe_sel_eqn;
+      fun rewrite bound_Ts U T (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) U T b)
+        | rewrite bound_Ts U T (t as _ $ _) =
+          let val (u, vs) = strip_comb t in
+            if is_Free u andalso has_call u then
+              Inr_const U T $ mk_tuple1 bound_Ts vs
+            else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
+              map (rewrite bound_Ts U T) vs |> chop 1 |>> HOLogic.mk_split o the_single |> list_comb
+            else
+              list_comb (rewrite bound_Ts U T u, map (rewrite bound_Ts U T) vs)
+          end
+        | rewrite _ U T t =
+          if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t;
+      fun massage t =
         massage_indirect_corec_call lthy has_call rewrite [] (range_type (fastype_of t)) rhs_term
         |> abs_tuple fun_args;
-  in
-    massage maybe_sel_eqn
+    in
+      massage
+    end
   end;
 
 fun build_corec_args_sel lthy has_call all_sel_eqns ctr_spec =

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 20:29:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 21:25:53 2013 +0200
@@ -149,8 +149,6 @@
 fun s_not @{const True} = @{const False}
   | s_not @{const False} = @{const True}
   | s_not (@{const Not} $ t) = t
-  (* TODO: is the next case really needed? *)
-  | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
   | s_not t = HOLogic.mk_not t
 
 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};