--- 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;