@@ -28,8 +28,8 @@ mkPatTm t = do i <- getIState
2828 evalStateT (toTT (mapPT deNS timp)) 0
2929 where
3030 toTT (PRef _ n) = do i <- lift getIState
31− case lookupDef n (tt_ctxt i) of
32− [TyDecl nt _] -> return $ P nt n Erased
31+ case lookupNameDef n (tt_ctxt i) of
32+ [(n', TyDecl nt _)] -> return $ P nt n' Erased
3333 _ -> return $ P Ref n Erased
3434 toTT (PApp _ t args) = do t' <- toTT t
3535 args' <- mapM (toTT . getTm) args