@@ -404,9 +404,8 @@ mutual
404404 withNInj Refl = (Refl, Refl)
405405
406406 private
407− instanceNInj : (InstanceN n xs = InstanceN n' ys) -> (n = n', xs = ys)
407+ instanceNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)
408408 instanceNInj Refl = (Refl, Refl)
409− %deprecate instanceNInj "`instanceNInj` is deprecated, Please use `implementationNInj` instead."
410409
411410 private
412411 implementationNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)
@@ -577,6 +576,9 @@ mutual
577576 decSNEq (MetaN n n') (MetaN x y) | No contra =
578577 No $ contra . fst . metaNInj
579578
579+-- (Temporarily?) Outside the mutual block, since otherwise we get the
580+-- warning on the second pass!
581+%deprecate instanceNInj "`instanceNInj` is deprecated, Please use `implementationNInj` instead."
580582
581583implementation DecEq TTName where
582584 decEq = decTTNameEq