# HG changeset patch
# User blanchet
# Date 1380127777 -7200
# Node ID e5dedcbd823b90abca3ca3c273356d3145b4d183
# Parent  d2d93b736e56869e1f850efc1c4757875f650085
don't generate wrong type

diff -r d2d93b736e56 -r e5dedcbd823b src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 18:00:53 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 18:49:37 2013 +0200
@@ -232,15 +232,18 @@
       | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
         fld (conds @ HOLogic.conjuncts cond) then_branch
         o fld (conds @ s_not_disj cond) else_branch
-      | (Const (c, _), args as _ :: _) =>
-        let val n = num_binder_types (Sign.the_const_type thy c) in
-          (case fastype_of1 (bound_Ts, nth args (n - 1)) of
-            Type (s, Ts) =>
-            (case dest_case ctxt s Ts t of
-              NONE => f conds t
-            | SOME (conds', branches) =>
-              fold_rev (uncurry fld) (map (append conds o HOLogic.conjuncts) conds' ~~ branches))
-          | _ => f conds t)
+      | (Const (c, _), args as _ :: _ :: _) =>
+        let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
+          if length args > n then
+            (case fastype_of1 (bound_Ts, nth args n) of
+              Type (s, Ts) =>
+              (case dest_case ctxt s Ts t of
+                NONE => f conds t
+              | SOME (conds', branches) =>
+                fold_rev (uncurry fld) (map (append conds o HOLogic.conjuncts) conds' ~~ branches))
+            | _ => f conds t)
+          else
+            f conds t
         end
       | _ => f conds t)
   in
@@ -266,17 +269,22 @@
           let val branches' = map (massage_rec bound_Ts) branches in
             Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
           end
-        | (Const (c, _), args as _ :: _) =>
-          let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
-            if n < length args then
-              (case typof (nth args n) of
-                Type (s, Ts) =>
-                if case_of ctxt s = SOME c then
+        | (Const (c, _), args as _ :: _ :: _) =>
+          let
+            val gen_T = Sign.the_const_type thy c;
+            val (gen_branch_Ts, gen_body_fun_T) = strip_fun_type gen_T;
+            val n = length gen_branch_Ts;
+          in
+            if length args > n then
+              (case gen_body_fun_T of
+                Type (_, [Type (T_name, _), _]) =>
+                if case_of ctxt T_name = SOME c then
                   let
                     val (branches, obj_leftovers) = chop n args;
                     val branches' = map (massage_abs bound_Ts o Envir.eta_long bound_Ts) branches;
-                    val casex' = Const (c, map typof branches' ---> map typof obj_leftovers --->
-                      typof t);
+                    val branch_Ts' = map typof branches';
+                    val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers --->
+                      snd (strip_typeN (num_binder_types (hd gen_branch_Ts)) (hd branch_Ts')));
                   in
                     Term.list_comb (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
                   end