# HG changeset patch
# User blanchet
# Date 1376669698 -7200
# Node ID 7dd103c29f9d33a7f7021aa7370b67f43b3fe1c6
# Parent  b139670d88d929e14cc22b3862b2224fa1eb8536
added more functions to BNF library

diff -r b139670d88d9 -r 7dd103c29f9d src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:06:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:14:58 2013 +0200
@@ -75,6 +75,8 @@
     (string * sort) list * Proof.context
   val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
 
+  val binder_fun_types: typ -> typ list
+  val body_fun_type: typ -> typ
   val num_binder_types: typ -> int
   val strip_typeN: int -> typ -> typ list * typ
 
@@ -420,10 +422,17 @@
     1 + num_binder_types T2
   | num_binder_types _ = 0
 
+(*maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T)*)
 fun strip_typeN 0 T = ([], T)
   | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T
   | strip_typeN _ T = raise TYPE ("strip_typeN", [T], []);
 
+(*maps [T1,...,Tn]--->T-->U to ([T1,T2,...,Tn], T-->U), where U is not a function type*)
+fun strip_fun_type T = strip_typeN (num_binder_types T - 1) T;
+
+val binder_fun_types = fst o strip_fun_type;
+val body_fun_type = snd o strip_fun_type;
+
 fun mk_predT Ts = Ts ---> HOLogic.boolT;
 fun mk_pred1T T = mk_predT [T];
 fun mk_pred2T T U = mk_predT [T, U];