fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'

--- a/src/HOL/Library/RBT_Set.thy	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Thu Sep 11 18:54:36 2014 +0200
@@ -10,7 +10,7 @@
 
 (*
   Users should be aware that by including this file all code equations
-  outside of List.thy using 'a list as an implenentation of sets cannot be
+  outside of List.thy using 'a list as an implementation of sets cannot be
   used for code generation. If such equations are not needed, they can be
   deleted from the code generator. Otherwise, a user has to provide their 
   own equations using RBT trees. 

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Sep 11 18:54:36 2014 +0200
@@ -296,25 +296,27 @@
 
     fun subst bound_Ts (t as g' $ y) =
         let
-          fun subst_rec () = subst bound_Ts g' $ subst bound_Ts y;
+          fun subst_rec (h $ z) = subst bound_Ts h $ subst bound_Ts z
+            | subst_rec t = t;
+
           val y_head = head_of y;
         in
           if not (member (op =) ctr_args y_head) then
-            subst_rec ()
+            subst_rec t
           else
             (case try_nested_rec bound_Ts y_head t of
-              SOME t' => t'
+              SOME t' => subst_rec t'
             | NONE =>
               let val (g, g_args) = strip_comb g' in
                 (case try (get_ctr_pos o fst o dest_Free) g of
-                  SOME ~1 => subst_rec ()
+                  SOME ~1 => subst_rec t
                 | SOME ctr_pos =>
                   (length g_args >= ctr_pos orelse
                    raise PRIMREC ("too few arguments in recursive call", [t]);
                    (case AList.lookup (op =) mutual_calls y of
                      SOME y' => list_comb (y', g_args)
-                   | NONE => subst_rec ()))
-                | NONE => subst_rec ())
+                   | NONE => subst_rec t))
+                | NONE => subst_rec t)
               end)
         end
       | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)