# HG changeset patch
# User haftmann
# Date 1259577768 -3600
# Node ID e191b400a8e0a92731e853a66743d9d3f2bdfe03
# Parent  b863967f23eaff2b1948e5983276e8db3aff5d56
more accurate linerarity

diff -r b863967f23ea -r e191b400a8e0 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Mon Nov 30 08:08:31 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Mon Nov 30 11:42:48 2009 +0100
@@ -502,7 +502,7 @@
     val consts = Sign.consts_of thy;
     val improve_constraints = AList.lookup (op =)
       (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
-    fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
+    fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts
      of NONE => NONE
       | SOME ts' => SOME (ts', ctxt);
     val lookup_inst_param = AxClass.lookup_inst_param consts params;