# HG changeset patch
# User wenzelm
# Date 1144922471 -7200
# Node ID c7a2b7a8c4cbdf9454705f2861c968a45801ef46
# Parent  cae7cc0729946f9ad5a66f9ad53b0ef3448284b4
certify: ignore sort constraints of declarations (MAJOR CHANGE);

diff -r cae7cc072994 -r c7a2b7a8c4cb src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu Apr 13 12:01:10 2006 +0200
+++ b/src/Pure/consts.ML	Thu Apr 13 12:01:11 2006 +0200
@@ -144,12 +144,12 @@
               val T' = Type.cert_typ tsig T;
               val ((U, kind), _) = the_const consts c;
             in
-              if not (Type.typ_instance tsig (T', U)) then
+              if not (Type.raw_instance (T', U)) then
                 err "Illegal type for constant" (c, T)
               else
                 (case (kind, expand_abbrevs) of
                   (Abbreviation u, true) =>
-                    Term.betapplys (Envir.expand_atom tsig T' (U, u) handle TYPE _ =>
+                    Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ =>
                       err "Illegal type for abbreviation" (c, T), map cert args)
                 | _ => comb head)
             end