@@ -2053,8 +2053,10 @@ elabDecl' what info d@(PClauses f o n ps)
20532053 [] -> []
20542054 elabClauses info f (o ++ o') n ps
20552055elabDecl' what info (PMutual f ps)
2056− = do mapM_ (elabDecl ETypes info) ps
2057− mapM_ (elabDecl EDefns info) ps
2056+ = do case ps of
2057+ [p] -> elabDecl what info p
2058+ _ -> do mapM_ (elabDecl ETypes info) ps
2059+ mapM_ (elabDecl EDefns info) ps
20582060 -- Do totality checking after entire mutual block
20592061 i <- get
20602062 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n