diff --git a/src/Core/CaseTree.hs b/src/Core/CaseTree.hs
index 7fb5e5575..349e14f63 100644
--- a/src/Core/CaseTree.hs
+++ b/src/Core/CaseTree.hs
@@ -158,7 +158,8 @@ data Phase = CompileTime | RunTime
 -- Generate a simple case tree
 -- Work Left to Right at Compile Time 
 
-simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] -> TC CaseDef
+simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] -> 
+              TC CaseDef
 simpleCase tc cover phase fc [] 
                  = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []
 simpleCase tc cover phase fc cs 
diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs
index e1ab72023..797bf5268 100644
--- a/src/Idris/ElabDecls.hs
+++ b/src/Idris/ElabDecls.hs
@@ -320,7 +320,6 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
                        else stripCollapsed pats
 
          logLvl 5 $ "Patterns:\n" ++ show pats
-         logLvl 5 $ "Optimised patterns:\n" ++ show optpats
 
          let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats
          tree@(CaseDef scargs sc _) <- tclift $ 
@@ -339,6 +338,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
                     else return []
          let pcover = null pmissing
          pdef' <- applyOpts optpdef 
+         logLvl 5 $ "Optimised patterns:\n" ++ show pdef'
          ist <- get
 --          let wf = wellFounded ist n sc
          let tot = if pcover || AssertTotal `elem` opts
@@ -400,7 +400,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
     
     getLHS (_, l, _) = l
 
-    simpl rt ctxt (Right (x, y)) = Right (x, simplify ctxt rt [] y)
+    simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x, 
+                                          simplify ctxt rt [] y)
     simpl rt ctxt t = t
 
     sameLength ((_, x, _) : xs) 
diff --git a/test/reg005/expected b/test/reg005/expected
new file mode 100644
index 000000000..42b01a14b
--- /dev/null
+++ b/test/reg005/expected
@@ -0,0 +1 @@
+1f4o1b4a1r1b3a1z
diff --git a/test/reg005/reg005.idr b/test/reg005/reg005.idr
new file mode 100644
index 000000000..ed48a3843
--- /dev/null
+++ b/test/reg005/reg005.idr
@@ -0,0 +1,50 @@
+module Main
+
+rep : (n : Nat) -> Char -> Vect Char n
+rep O     x = []
+rep (S k) x = x :: rep k x
+
+data RLE : Vect Char n -> Set where
+     REnd  : RLE []
+     RChar : {xs : Vect Char k} ->
+             (n : Nat) -> (x : Char) -> RLE xs -> 
+             RLE (rep (S n) x ++ xs)
+
+eq : (x : Char) -> (y : Char) -> Maybe (x = y)
+eq x y = if x == y then Just ?eqCharOK else Nothing
+
+------------
+
+rle : (xs : Vect Char n) -> RLE xs
+rle [] = REnd
+rle (x :: xs) with (rle xs)
+   rle (x :: [])            | REnd = RChar O x REnd 
+   rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)
+     rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just p 
+           = RChar (S n) x rs
+     rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing 
+           = RChar O x (RChar n y rs)
+
+compress : Vect Char n -> String
+compress xs with (rle xs)
+  compress Nil                 | REnd         = ""
+  compress (rep (S n) x ++ xs) | RChar n x rs 
+         = let ni : Int = cast (S n) in
+               show ni ++ show x ++ compress xs
+
+compressString : String -> String
+compressString xs = compress (fromList (unpack xs))
+
+main : IO ()
+main = putStrLn (compressString "foooobaaaarbaaaz")
+
+
+
+---------- Proofs ----------
+
+Main.eqCharOK = proof {
+  intros;
+  refine believe_me;
+  exact x = x;
+}
+
diff --git a/test/reg005/run b/test/reg005/run
new file mode 100755
index 000000000..84ace247a
--- /dev/null
+++ b/test/reg005/run
@@ -0,0 +1,4 @@
+#!/bin/bash
+idris $@ reg005.idr -o reg005
+./reg005
+rm -f reg005 *.ibc