@@ -361,16 +361,19 @@ getProofClause l fn fp
361361
362362mkWith :: String -> Name -> String
363363mkWith str n = let str' = replaceRHS str "with (_)"
364− newpat = " " ++
365− replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
366− str' ++ "\n" ++ newpat
364+ in str' ++ "\n" ++ newpat str
367365
368366 where replaceRHS [] str = str
369367 replaceRHS ('?':'=': rest) str = str
370− replaceRHS ('=': rest) str
368+ replaceRHS ('=': rest) str
371369 | not ('=' `elem` rest) = str
372370 replaceRHS (x : rest) str = x : replaceRHS rest str
373371
372+ newpat ('>':patstr) = '>':newpat patstr
373+ newpat patstr =
374+ " " ++
375+ replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"
376+
374377-- Replace _ with names in missing clauses
375378
376379nameMissing :: [PTerm] -> Idris [PTerm]