added forall2 predicate lifter

--- a/src/Pure/Isar/code.ML	Mon Nov 15 22:31:18 2010 +0100
+++ b/src/Pure/Isar/code.ML	Tue Nov 16 10:33:36 2010 +0100
@@ -565,7 +565,7 @@
       else bad ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
     val _ = check_eqn thy { allow_nonlinear = false,
       allow_consts = false, allow_pats = false } thm (lhs, rhs);
-    val _ = if forall (Sign.of_sort thy) (Ts ~~ map snd vs') then ()
+    val _ = if forall2 (fn T => fn (_, sort) => Sign.of_sort thy (T, sort)) Ts vs' then ()
       else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   in (thm, tyco) end;
 

--- a/src/Pure/library.ML	Mon Nov 15 22:31:18 2010 +0100
+++ b/src/Pure/library.ML	Tue Nov 16 10:33:36 2010 +0100
@@ -97,6 +97,7 @@
   val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+  val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   val zip_options: 'a list -> 'b option list -> ('a * 'b) list
   val ~~ : 'a list * 'b list -> ('a * 'b) list
   val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
@@ -543,6 +544,10 @@
   | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
   | fold2 f _ _ _ = raise UnequalLengths;
 
+fun forall2 P [] [] = true
+  | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
+  | forall2 P _ _ = false;
+
 fun map_split f [] = ([], [])
   | map_split f (x :: xs) =
       let

--- a/src/Tools/nbe.ML	Mon Nov 15 22:31:18 2010 +0100
+++ b/src/Tools/nbe.ML	Tue Nov 16 10:33:36 2010 +0100
@@ -170,11 +170,10 @@
   | Abs of (int * (Univ list -> Univ)) * Univ list
                                        (*abstractions as closures*);
 
-fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso sames xs ys
+fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso forall2 same xs ys
   | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
-  | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso sames xs ys
-  | same _ _ = false
-and sames xs ys = length xs = length ys andalso forall (uncurry same) (xs ~~ ys);
+  | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso forall2 same xs ys
+  | same _ _ = false;
 
 
 (* constructor functions *)