@@ -361,16 +361,19 @@ getProofClause l fn fp
362mkWith :: String -> Name -> String
362mkWith :: String -> Name -> String
363mkWith str n = let str' = replaceRHS str "with (_)"
363mkWith str n = let str' = replaceRHS str "with (_)"
365− replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
366− str' ++ "\n" ++ newpat
364+ in str' ++ "\n" ++ newpat str
368 where replaceRHS [] str = str
366 where replaceRHS [] str = str
369 replaceRHS ('?':'=': rest) str = str
367 replaceRHS ('?':'=': rest) str = str
370− replaceRHS ('=': rest) str
368+ replaceRHS ('=': rest) str
371 | not ('=' `elem` rest) = str
369 | not ('=' `elem` rest) = str
372 replaceRHS (x : rest) str = x : replaceRHS rest str
370 replaceRHS (x : rest) str = x : replaceRHS rest str
372+ newpat ('>':patstr) = '>':newpat patstr
375+ replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"
374-- Replace _ with names in missing clauses
377-- Replace _ with names in missing clauses
376nameMissing :: [PTerm] -> Idris [PTerm]
379nameMissing :: [PTerm] -> Idris [PTerm]