# HG changeset patch
# User blanchet
# Date 1382622963 -7200
# Node ID 20a52b55f8ea2187d11fad272cc0a92ab902532d
# Parent  4fadf746f2d512b9ba71beb8713fb45f56746903
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')

diff -r 4fadf746f2d5 -r 20a52b55f8ea src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 24 15:32:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 24 15:56:03 2013 +0200
@@ -317,8 +317,7 @@
       (case Term.strip_comb t of
         (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_let t)
       | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
-        fld (conds @ conjuncts_s cond) then_branch
-        o fld (conds @ s_not_conj [cond]) else_branch
+        fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch
       | (Const (c, _), args as _ :: _ :: _) =>
         let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
           if n >= 0 andalso n < length args then
@@ -361,30 +360,32 @@
             Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
           end
         | (Const (c, _), args as _ :: _ :: _) =>
-          let
-            val gen_T = Sign.the_const_type thy c;
-            val (gen_branch_ms, gen_body_fun_T) = strip_fun_type gen_T |>> map num_binder_types;
-            val n = length gen_branch_ms;
-          in
-            if n < length args 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' = map2 (massage_abs bound_Ts) gen_branch_ms branches;
-                    val branch_Ts' = map typof branches';
-                    val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts'));
-                    val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T');
-                  in
-                    Term.list_comb (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
-                  end
-                else
-                  massage_leaf bound_Ts t
-              | _ => massage_leaf bound_Ts t)
-            else
-              massage_leaf bound_Ts t
-          end
+          (case try strip_fun_type (Sign.the_const_type thy c) of
+            SOME (gen_branch_Ts, gen_body_fun_T) =>
+            let
+              val gen_branch_ms = map num_binder_types gen_branch_Ts;
+              val n = length gen_branch_ms;
+            in
+              if n < length args 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' = map2 (massage_abs bound_Ts) gen_branch_ms branches;
+                      val branch_Ts' = map typof branches';
+                      val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts'));
+                      val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T');
+                    in
+                      Term.list_comb (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
+                    end
+                  else
+                    massage_leaf bound_Ts t
+                | _ => massage_leaf bound_Ts t)
+              else
+                massage_leaf bound_Ts t
+            end
+          | NONE => massage_leaf bound_Ts t)
         | _ => massage_leaf bound_Ts t)
       end
   in