improved massaging of case expressions

--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 25 16:43:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 25 16:43:46 2013 +0200
@@ -42,6 +42,7 @@
   val mk_disc_or_sel: typ list -> term -> term
   val name_of_ctr: term -> string
   val name_of_disc: term -> string
+  val dest_ctr: Proof.context -> string -> term -> term * term list
   val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
 
   val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
@@ -215,6 +216,18 @@
 
 val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
 
+fun dest_ctr ctxt s t =
+  let
+    val (f, args) = Term.strip_comb t;
+  in
+    (case ctr_sugar_of ctxt s of
+      SOME {ctrs, ...} =>
+      (case find_first (can (fo_match ctxt f)) ctrs of
+        SOME f' => (f', args)
+      | NONE => raise Fail "dest_ctr")
+    | NONE => raise Fail "dest_ctr")
+  end;
+
 fun dest_case ctxt s Ts t =
   (case Term.strip_comb t of
     (Const (c, _), args as _ :: _) =>

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Sep 25 16:43:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Sep 25 16:43:46 2013 +0200
@@ -319,11 +319,6 @@
 
 end;
 
-fun fo_match ctxt t pat =
-  let val thy = Proof_Context.theory_of ctxt in
-    Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
-  end;
-
 val dummy_var_name = "?f"
 
 fun mk_map_pattern ctxt s =
@@ -345,18 +340,6 @@
     (map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv [])
   end;
 
-fun dest_ctr ctxt s t =
-  let
-    val (f, args) = Term.strip_comb t;
-  in
-    (case fp_sugar_of ctxt s of
-      SOME fp_sugar =>
-      (case find_first (can (fo_match ctxt f)) (#ctrs (of_fp_sugar #ctr_sugars fp_sugar)) of
-        SOME f' => (f', args)
-      | NONE => raise Fail "dest_ctr")
-    | NONE => raise Fail "dest_ctr")
-  end;
-
 fun liveness_of_fp_bnf n bnf =
   (case T_of_bnf bnf of
     Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:43:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:43:46 2013 +0200
@@ -251,24 +251,28 @@
 
 fun massage_let_if_case ctxt has_call massage_leaf bound_Ts U =
   let
+    val thy = Proof_Context.theory_of ctxt;
+
     val typof = curry fastype_of1 bound_Ts;
-    val check_obj = ((not o has_call) orf unexpected_corec_call ctxt);
+    fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
 
     fun massage_rec t =
       (case Term.strip_comb t of
         (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec (betapply (arg2, arg1))
       | (Const (@{const_name If}, _), obj :: branches) =>
-        Term.list_comb (If_const U $ tap check_obj obj, map massage_rec branches)
+        Term.list_comb (If_const U $ tap check_no_call obj, map massage_rec branches)
       | (Const (c, _), args as _ :: _) =>
-        let val (branches, obj) = split_last args in
-          (case fastype_of1 (bound_Ts, obj) of
-            Type (T_name, _) =>
-            if case_of ctxt T_name = SOME c then
+        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) =>
+            if case_of ctxt s = SOME c then
               let
+                val (branches, obj_leftovers) = chop n args;
                 val branches' = map massage_rec branches;
-                val casex' = Const (c, map typof branches' ---> typof obj);
+                val casex' = Const (c, map typof branches' ---> map typof obj_leftovers --->
+                  typof t);
               in
-                Term.list_comb (casex', branches') $ tap check_obj obj
+                betapplys (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
               end
             else
               massage_leaf t

--- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 25 16:43:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 25 16:43:46 2013 +0200
@@ -134,6 +134,8 @@
   val list_all_free: term list -> term -> term
   val list_exists_free: term list -> term -> term
 
+  val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv
+
   (*parameterized terms*)
   val mk_nthN: int -> term -> int -> term
 
@@ -645,6 +647,11 @@
 val list_all_free = list_quant_free HOLogic.all_const;
 val list_exists_free = list_quant_free HOLogic.exists_const;
 
+fun fo_match ctxt t pat =
+  let val thy = Proof_Context.theory_of ctxt in
+    Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
+  end;
+
 fun find_indices eq xs ys = map_filter I
   (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys);