@@ -683,10 +683,6 @@ process h fn (NewDefn decls) = do
683683 getClauseName (PClause fc name whole with rhs whereBlock) = name
684684 getClauseName (PWith fc name whole with rhs whereBlock) = name
685685 defineName :: [PDecl] -> Idris ()
686− defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do
687− elabDecl EAll toplevel tyDecl
688− elabClauses toplevel fc opts name (concatMap getClauses decls)
689− setReplDefined (Just name)
690686 defineName [PClauses fc opts _ [clause]] = do
691687 let pterm = getRHS clause
692688 (tm,ty) <- elabVal toplevel ERHS pterm