--- 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