# HG changeset patch
# User wenzelm
# Date 1144922473 -7200
# Node ID d7c10da57042692babf0dcab72e0453272e8b884
# Parent  87cbbe045ea5e067d9de22e1b7638d6c8a969900
ignore sort constraints of consts declarations;
Sign.typ_equiv;

diff -r 87cbbe045ea5 -r d7c10da57042 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Thu Apr 13 12:01:12 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Thu Apr 13 12:01:13 2006 +0200
@@ -127,13 +127,9 @@
 
 type deftab = (typ * thm) list Symtab.table;
 
-fun eq_typ thy (ty1, ty2) =
-  Sign.typ_instance thy (ty1, ty2)
-    andalso Sign.typ_instance thy (ty2, ty1);
-
 fun is_overloaded thy c = case Defs.specifications_of (Theory.defs_of thy) c
  of [] => true
-  | [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c))
+  | [(ty, _)] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c))
   | _ => true;
 
 structure InstNameMangler = NameManglerFun (
@@ -156,7 +152,7 @@
     let
       val c' = idf_of_name thy nsp_overl c;
       val prefix = 
-        case (AList.lookup (eq_typ thy)
+        case (AList.lookup (Sign.typ_equiv thy)
             (Defs.specifications_of (Theory.defs_of thy) c)) ty
          of SOME (_, thyname) => NameSpace.append thyname nsp_overl
           | NONE => if c = "op ="
@@ -173,7 +169,7 @@
             NONE
     in
       Vartab.empty
-      |> Sign.typ_match thy (Sign.the_const_type thy c, ty)
+      |> Type.raw_match (Sign.the_const_type thy c, ty)
       |> map (snd o snd) o Vartab.dest
       |> List.mapPartial mangle
       |> Library.flat
@@ -938,7 +934,7 @@
               val is_overl = (is_none o ClassPackage.lookup_const_class thy) c
                andalso case deftab
                of [] => false
-                | [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c))
+                | [(ty, _)] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c))
                 | _ => true;
             in if is_overl then (fn (overltab1, overltab2) => (
               overltab1