# HG changeset patch
# User haftmann
# Date 1242826513 -7200
# Node ID b67179528acddfd2e1a9dc9b409d8cb9c6fe6523
# Parent  800787c3210fbdbe288c2fa140308c71d5390eef
tuned

diff -r 800787c3210f -r b67179528acd src/Pure/Isar/class_target.ML
--- 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)