diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs
index 21fc5126..e5f9eaa7 100644
--- a/src/Cryptol/Parser/NoPat.hs
+++ b/src/Cryptol/Parser/NoPat.hs
@@ -162,8 +162,7 @@ noPatE expr =
     EWhere e ds   -> EWhere <$> noPatE e <*> noPatDs ds
     ETyped e t    -> ETyped <$> noPatE e <*> return t
     ETypeVal {}   -> return expr
-    EFun ps e     -> do (ps1,e1) <- noPatFun ps e
-                        return (EFun ps1 e1)
+    EFun ps e     -> noPatFun ps e
     ELocated e r1 -> ELocated <$> inRange r1 (noPatE e) <*> return r1
 
     ESplit e      -> ESplit  <$> noPatE e
@@ -174,15 +173,25 @@ noPatE expr =
 noPatUF :: UpdField PName -> NoPatM (UpdField PName)
 noPatUF (UpdField h ls e) = UpdField h ls <$> noPatE e
 
-noPatFun :: [Pattern PName] -> Expr PName -> NoPatM ([Pattern PName], Expr PName)
-noPatFun ps e =
-  do (xs,bs) <- unzip <$> mapM noPat ps
-     e1 <- noPatE e
-     let body = case concat bs of
-                        [] -> e1
-                        ds -> EWhere e1 $ map DBind ds
-     return (xs, body)
-
+-- Desugar lambdas with multiple patterns into a sequence of
+-- lambdas with a single, simple pattern each.  Bindings required
+-- to simplify patterns are placed inside "where" blocks that are
+-- interspersed into the lambdas to ensure that the lexical
+-- structure is reliable, with names on the right shadowing names
+-- on the left.
+noPatFun :: [Pattern PName] -> Expr PName -> NoPatM (Expr PName)
+noPatFun [] e = noPatE e
+noPatFun (p:ps) e =
+  do (p',ds) <- noPat p
+     e' <- noPatFun ps e
+     let body = case ds of
+                  [] -> e'
+                  _  -> EWhere e' $ map DBind (reverse ds)
+                           --                  ^
+                           -- This reverse isn't strictly necessary, but yields more sensible
+                           -- variable ordering results from type inference.  I'm not entirely
+                           -- sure why.
+     return (EFun [p'] body)
 
 noPatArm :: [Match PName] -> NoPatM [Match PName]
 noPatArm ms = concat <$> mapM noPatM ms
@@ -203,8 +212,8 @@ noMatchB b =
                                               , show b ]
 
     DExpr e ->
-      do (ps,e') <- noPatFun (bParams b) e
-         return b { bParams = ps, bDef = DExpr e' <$ bDef b }
+      do e' <- noPatFun (bParams b) e
+         return b { bParams = [], bDef = DExpr e' <$ bDef b }
 
 noMatchD :: Decl PName -> NoPatM [Decl PName]
 noMatchD decl =
diff --git a/tests/issues/issue567.icry.stdout b/tests/issues/issue567.icry.stdout
index 29b5f200..2e56bafe 100644
--- a/tests/issues/issue567.icry.stdout
+++ b/tests/issues/issue567.icry.stdout
@@ -2,28 +2,26 @@ Loading module Cryptol
 [warning] at issue567.icry:1:7--1:8
     This binding for `x` shadows the existing binding at
     issue567.icry:1:5--1:6
-(\x x -> x : [8]) : {a} [8] -> a -> [8]
+(\x x -> x : [8]) : {a} a -> [8] -> [8]
 [warning] at issue567.icry:2:11--2:12
     This binding for `x` shadows the existing binding at
     issue567.icry:2:5--2:6
 (\x -> \x -> x : [8]) : {a} a -> [8] -> [8]
-[warning] at issue567.icry:3:6--3:7
+[warning] at issue567.icry:3:12--3:13
     This binding for `x` shadows the existing binding at
-    issue567.icry:3:12--3:13
-(\(x, y) x -> x) : {a, b, c} (c, b) -> a -> c
-
-[error]
-    Overlapping symbols defined:
-    (at issue567.icry:4:6--4:7, x)
-    (at issue567.icry:4:13--4:14, x)
-[error]
-    Overlapping symbols defined:
-    (at issue567.icry:4:9--4:10, y)
-    (at issue567.icry:4:16--4:17, y)
-[warning] at issue567.icry:5:11--5:12
+    issue567.icry:3:6--3:7
+(\(x, y) x -> x) : {a, b, c} (a, b) -> c -> c
+[warning] at issue567.icry:4:16--4:17
+    This binding for `y` shadows the existing binding at
+    issue567.icry:4:9--4:10
+[warning] at issue567.icry:4:13--4:14
     This binding for `x` shadows the existing binding at
-    issue567.icry:5:5--5:6
+    issue567.icry:4:6--4:7
+(\(x, y) (x, y) -> x) : {a, b, c, d} (a, b) -> (c, d) -> c
 [warning] at issue567.icry:5:8--5:9
     This binding for `x` shadows the existing binding at
     issue567.icry:5:5--5:6
-(\x [x] x -> x) : {a, b, c} a -> [1]c -> b -> c
+[warning] at issue567.icry:5:11--5:12
+    This binding for `x` shadows the existing binding at
+    issue567.icry:5:8--5:9
+(\x [x] x -> x) : {a, b, c} a -> [1]b -> c -> c