src/Pure/Isar/class_target.ML
changeset 31214 b67179528acd
parent 31210 d6681ddc046c
child 31249 d51d2a22a4f9
--- a/src/Pure/Isar/class_target.ML	Wed May 20 15:35:13 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed May 20 15:35:13 2009 +0200
@@ -512,7 +512,7 @@
     fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
      of NONE => NONE
       | SOME ts' => SOME (ts', ctxt);
-    val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of thy);
+    val inst_tyco_of = AxClass.inst_tyco_of consts;
     val typ_instance = Type.typ_instance (Sign.tsig_of thy);
     fun improve (c, ty) = case inst_tyco_of (c, ty)
      of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)