src/Pure/Isar/class_target.ML
changeset 33967 e191b400a8e0
parent 33671 4b0f2599ed48
child 33969 1e7ca47c6c3d
     1.1 --- a/src/Pure/Isar/class_target.ML	Mon Nov 30 08:08:31 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Mon Nov 30 11:42:48 2009 +0100
     1.3 @@ -502,7 +502,7 @@
     1.4      val consts = Sign.consts_of thy;
     1.5      val improve_constraints = AList.lookup (op =)
     1.6        (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
     1.7 -    fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
     1.8 +    fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts
     1.9       of NONE => NONE
    1.10        | SOME ts' => SOME (ts', ctxt);
    1.11      val lookup_inst_param = AxClass.lookup_inst_param consts params;