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