# HG changeset patch
# User haftmann
# Date 1288098042 -7200
# Node ID 9b6e918682d577215bfd9476534699aff4c9aab6
# Parent  fe4a58419d46845acf61f901a98cb2507a3e8f7e
more general treatment of type argument in code certificates for operations on abstract types

diff -r fe4a58419d46 -r 9b6e918682d5 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Oct 26 14:11:34 2010 +0200
+++ b/src/Pure/Isar/code.ML	Tue Oct 26 15:00:42 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);