# HG changeset patch
# User traytel
# Date 1347784405 -7200
# Node ID 323414474c1f68a87981fd53588747c7f4a105ad
# Parent  52e636ace94e19da5d572f8fd2b7a89b56de1172
use strip_typeN in bnf_def (instead of repairing strip_type)

diff -r 52e636ace94e -r 323414474c1f src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Sun Sep 16 06:51:36 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Sun Sep 16 10:33:25 2012 +0200
@@ -604,15 +604,14 @@
 
     val bnf_map = Morphism.term phi bnf_map_term;
 
-    fun iter_split ((Ts, T1), T2) = if length Ts < live then error "Bad map function"
-      else if length Ts = live then ((Ts, T1), T2)
-      else iter_split (split_last Ts, T1 --> T2);
-
     (*TODO: handle errors*)
     (*simple shape analysis of a map function*)
-    val (((alphas, betas), CA), _) =
-      apfst (apfst (map_split dest_funT))
-        (iter_split (apfst split_last (strip_type (fastype_of bnf_map))));
+    val ((alphas, betas), (CA, _)) =
+      fastype_of bnf_map
+      |> strip_typeN live
+      |>> map_split dest_funT
+      ||> dest_funT
+      handle TYPE _ => error "Bad map function";
 
     val CA_params = map TVar (Term.add_tvarsT CA []);
 
diff -r 52e636ace94e -r 323414474c1f src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 16 06:51:36 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 16 10:33:25 2012 +0200
@@ -92,7 +92,6 @@
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
-  val strip_typeN: int -> typ -> typ list * typ
   val retype_free: typ -> term -> term
 
   val mk_predT: typ -> typ;
@@ -241,9 +240,6 @@
 
 val mk_common_name = space_implode "_" o map Binding.name_of;
 
-fun strip_typeN 0 T = ([], T)
-  | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T;
-
 fun mk_predT T = T --> HOLogic.boolT;
 
 fun retype_free T (Free (s, _)) = Free (s, T);
diff -r 52e636ace94e -r 323414474c1f src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Sun Sep 16 06:51:36 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Sun Sep 16 10:33:25 2012 +0200
@@ -59,6 +59,8 @@
   val mk_Freess': string -> typ list list -> Proof.context ->
     (term list list * (string * typ) list list) * Proof.context
 
+  val strip_typeN: int -> typ -> typ list * typ
+
   val mk_optionT: typ -> typ
   val mk_relT: typ * typ -> typ
   val dest_relT: typ -> typ * typ
@@ -302,6 +304,10 @@
 
 (** Types **)
 
+fun strip_typeN 0 T = ([], T)
+  | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T
+  | strip_typeN n T = raise TYPE ("strip_typeN", [T], []);
+
 fun mk_optionT T = Type (@{type_name option}, [T]);
 val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT;
 val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT;