diff -r 88f6d5b1422f -r a2d18fea844a src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Tue Nov 12 14:00:56 2013 +0100
@@ -27,6 +27,8 @@
   val dest_binop_list: string -> term -> term list
   val regroup_conv: string -> string -> thm list -> int list -> conv
   val regroup_union_conv: int list -> conv
+
+  val inst_constrs_of : theory -> typ -> term list
 end
 
 structure Function_Lib: FUNCTION_LIB =
@@ -48,9 +50,7 @@
   | dest_all_all t = ([],t)
 
 
-fun map4 _ [] [] [] [] = []
-  | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
-  | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
+fun map4 f = Ctr_Sugar_Util.map4 f
 
 fun map7 _ [] [] [] [] [] [] [] = []
   | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
@@ -133,4 +133,10 @@
       (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left}))
 
 
+fun inst_constrs_of thy (T as Type (name, _)) =
+  map (fn CnCT as (_, CT) =>
+          Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const CnCT))
+      (the (Datatype.get_constrs thy name))
+  | inst_constrs_of thy _ = raise Match
+
 end