# 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)