Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorhaftmann
Wed, 20 May 2009 15:35:13 +0200
changeset 31214 b67179528acd
parent 31213 800787c3210f
child 31215 052fddd64006
tuned
src/Pure/Isar/class_target.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle