# HG changeset patch
# User blanchet
# Date 1288098062 -7200
# Node ID c60935e30171ff72b465005fefe51fcfefd5d02b
# Parent  9b6e918682d577215bfd9476534699aff4c9aab6# Parent  257d2e06bfb84842e78a8d5ac8220730406c6725
merged

diff -r 257d2e06bfb8 -r c60935e30171 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Oct 26 14:49:48 2010 +0200
+++ b/src/Pure/Isar/code.ML	Tue Oct 26 15:01:02 2010 +0200
@@ -542,7 +542,7 @@
     val (rep, lhs) = dest_comb full_lhs
       handle TERM _ => bad "Not an abstract equation";
     val (rep_const, ty) = dest_Const rep;
-    val (tyco, sorts) = ((apsnd o map) (snd o dest_TVar) o dest_Type o domain_type) ty
+    val (tyco, Ts) = (dest_Type o domain_type) ty
       handle TERM _ => bad "Not an abstract equation"
            | TYPE _ => bad "Not an abstract equation";
     val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
@@ -553,8 +553,8 @@
       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.subsort thy) (sorts ~~ map snd  vs') then ()
-      else error ("Sort constraints on type arguments are weaker than in abstype certificate.")
+    val _ = if forall (Sign.of_sort thy) (Ts ~~ map snd vs') then ()
+      else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   in (thm, tyco) end;
 
 fun assert_eqn thy = error_thm (gen_assert_eqn thy true);