@@ -1142,7 +1142,7 @@ showImp ist impl colour tm = se 10 [] tm where
1142 se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
1142 se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
1143 where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
1143 where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
1144 se p bnd (PHidden tm) = "." ++ se 0 bnd tm
1144 se p bnd (PHidden tm) = "." ++ se 0 bnd tm
1145− se p bnd (PRefl _ t)
1145+ se p bnd (PRefl _ t)
1146 | not impl = perhapsColourise colouriseData "refl"
1146 | not impl = perhapsColourise colouriseData "refl"
1147 | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"
1147 | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"
1148 se p bnd (PResolveTC _) = "resolvetc"
1148 se p bnd (PResolveTC _) = "resolvetc"