# HG changeset patch
# User blanchet
# Date 1384261256 -3600
# Node ID a2d18fea844a386bb404e30e892519c523320e5b
# Parent  88f6d5b1422f736a55c55c51e959e7a960ad42c8
undid copy-paste

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
diff -r 88f6d5b1422f -r a2d18fea844a src/HOL/Tools/Function/pat_completeness.ML
--- a/src/HOL/Tools/Function/pat_completeness.ML	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Tue Nov 12 14:00:56 2013 +0100
@@ -54,13 +54,6 @@
     else filter_pats thy cons pvars pts
 
 
-fun inst_constrs_of thy (T as Type (name, _)) =
-  map (fn (Cn,CT) =>
-          Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
-      (the (Datatype.get_constrs thy name))
-  | inst_constrs_of thy _ = raise Match
-
-
 fun transform_pat _ avars c_assum ([] , thm) = raise Match
   | transform_pat ctxt avars c_assum (pat :: pats, thm) =
   let
diff -r 88f6d5b1422f -r a2d18fea844a src/HOL/Tools/Function/pattern_split.ML
--- a/src/HOL/Tools/Function/pattern_split.ML	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Tools/Function/pattern_split.ML	Tue Nov 12 14:00:56 2013 +0100
@@ -30,14 +30,6 @@
     (binder_types (fastype_of t)) (vs, t)
 
 
-(* This is copied from "pat_completeness.ML" *)
-fun inst_constrs_of thy (T as Type (name, _)) =
-  map (fn (Cn,CT) =>
-    Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
-    (the (Datatype.get_constrs thy name))
-  | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
-
-
 fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
 fun join_product (xs, ys) = map_product (curry join) xs ys
 
@@ -49,7 +41,7 @@
     fun pattern_subtract_subst_aux vs _ (Free v2) = []
       | pattern_subtract_subst_aux vs (v as (Free (_, T))) t' =
           let
-            fun foo constr =
+            fun aux constr =
               let
                 val (vs', t) = saturate ctxt vs constr
                 val substs = pattern_subtract_subst ctxt vs' t t'
@@ -57,7 +49,7 @@
                 map (fn (vs, subst) => (vs, (v,t)::subst)) substs
               end
           in
-            maps foo (inst_constrs_of (Proof_Context.theory_of ctxt) T)
+            maps aux (inst_constrs_of (Proof_Context.theory_of ctxt) T)
           end
      | pattern_subtract_subst_aux vs t t' =
          let