diff --git a/idris.cabal b/idris.cabal
index 9561027d1..adcfc80e4 100644
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.9.4
+Version:        0.9.4.2
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -45,7 +45,7 @@ Data-files:            rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h
                        rts/libtest.c
 Extra-source-files:    lib/Makefile  lib/*.idr lib/prelude/*.idr lib/network/*.idr
                        lib/control/monad/*.idr lib/language/*.idr
-                       tutorial/examples/*.idr
+                       tutorial/examples/*.idr lib/base.ipkg
                        rts/*.c rts/*.h rts/Makefile
 
 source-repository head
@@ -74,7 +74,7 @@ Executable     idris
 
                               IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,
                               IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,
-                              IRTS.Compiler,
+                              IRTS.Compiler, IRTS.CodegenJava, IRTS.BCImp,
 
                               Paths_idris
 
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
index c6dd69849..7da35728b 100644
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -705,13 +705,24 @@ addImpl' inpat env ist ptm = ai env ptm
 
 aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
 aiFn inpat True ist fc f []
-  = case lookupCtxt Nothing f (idris_implicits ist) of
-        [] -> Right $ PRef fc f
-        alts -> if (any (all imp) alts)
+  = case lookupDef Nothing f (tt_ctxt ist) of
+        [] -> Right $ PPatvar fc f
+        alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in
+                    -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $ 
+                    if (not (vname f) || tcname f 
+                           || any constructor alts || any allImp ialts)
                         then aiFn inpat False ist fc f [] -- use it as a constructor
-                        else Right $ PRef fc f
+                        else Right $ PPatvar fc f
     where imp (PExp _ _ _) = False
           imp _ = True
+          allImp [] = False
+          allImp xs = all imp xs
+          constructor (TyDecl (DCon _ _) _) = True
+          constructor _ = False
+
+          vname (UN n) = True -- non qualified
+          vname _ = False
+
 aiFn inpat expat ist fc f as
     | f `elem` primNames = Right $ PApp fc (PRef fc f) as
 aiFn inpat expat ist fc f as
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
index 0eeeb1e1b..e2ca78060 100644
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -342,6 +342,7 @@ updateNs ns t = mapPT updateRef t
 
 data PTerm = PQuote Raw
            | PRef FC Name
+           | PPatvar FC Name
            | PLam Name PTerm PTerm
            | PPi  Plicity Name PTerm PTerm
            | PLet Name PTerm PTerm PTerm 
@@ -650,6 +651,7 @@ prettyImp impl = prettySe 10
         text "![" $$ pretty r <> text "]"
       else
         text "![" <> pretty r <> text "]"
+    prettySe p (PPatvar fc n) = pretty n
     prettySe p (PRef fc n) =
       if impl then
         pretty n
@@ -825,6 +827,7 @@ prettyImp impl = prettySe 10
 showImp :: Bool -> PTerm -> String
 showImp impl tm = se 10 tm where
     se p (PQuote r) = "![" ++ show r ++ "]"
+    se p (PPatvar fc n) = show n
     se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
                                else showbasic n
       where showbasic n@(UN _) = show n
diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs
index 6ea9ef05f..ef60d3286 100644
--- a/src/Idris/ElabTerm.hs
+++ b/src/Idris/ElabTerm.hs
@@ -153,6 +153,7 @@ elab ist info pattern tcgen fn tm
         = trySeq as
         where trySeq [] = fail "All alternatives fail to elaborate"
               trySeq (x : xs) = try (elab' ina x) (trySeq xs)
+    elab' ina (PPatvar fc n) | pattern = patvar n
     elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)
                          = do ctxt <- get_context
                               let iscon = isConName Nothing n ctxt
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
index 1ad349a58..9b5345dde 100644
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -1087,6 +1087,9 @@ instance Binary PTerm where
                 PTactics x1 -> do putWord8 25
                                   put x1
                 PImpossible -> putWord8 27
+                PPatvar x1 x2 -> do putWord8 28
+                                    put x1
+                                    put x2
         get
           = do i <- getWord8
                case i of
@@ -1164,6 +1167,9 @@ instance Binary PTerm where
                    25 -> do x1 <- get
                             return (PTactics x1)
                    27 -> return PImpossible
+                   28 -> do x1 <- get
+                            x2 <- get
+                            return (PPatvar x1 x2)
                    _ -> error "Corrupted binary data for PTerm"
  
 instance (Binary t) => Binary (PTactic' t) where
diff --git a/test/test014/run b/test/test014/run
index f40eb7a34..b5c6825e5 100755
--- a/test/test014/run
+++ b/test/test014/run
@@ -1,4 +1,4 @@
 #!/bin/bash
 idris test014.idr -o test014
 ./test014
-rm -f test014 test014.ibc
+rm -f test014 resimp.ibc test014.ibc
diff --git a/test/test015/expected b/test/test015/expected
new file mode 100644
index 000000000..3a35edc05
--- /dev/null
+++ b/test/test015/expected
@@ -0,0 +1,3 @@
+00101010
+01011001
+010000011
diff --git a/test/test015/parity.idr b/test/test015/parity.idr
new file mode 100644
index 000000000..144172062
--- /dev/null
+++ b/test/test015/parity.idr
@@ -0,0 +1,28 @@
+module parity
+
+data Parity : Nat -> Set where
+   even : Parity (n + n)
+   odd  : Parity (S (n + n))
+
+parity : (n:Nat) -> Parity n
+parity O     = even {n=O}
+parity (S O) = odd {n=O}
+parity (S (S k)) with (parity k)
+    parity (S (S (j + j)))     | even ?= even {n=S j}
+    parity (S (S (S (j + j)))) | odd  ?= odd {n=S j}
+
+
+parity_lemma_2 = proof {
+    intro;
+    intro;
+    rewrite sym (plusSuccRightSucc j j);
+    trivial;
+}
+
+parity_lemma_1 = proof {
+    intro j;
+    intro;
+    rewrite sym (plusSuccRightSucc j j);
+    trivial;
+}
+
diff --git a/test/test015/run b/test/test015/run
new file mode 100755
index 000000000..66896a86c
--- /dev/null
+++ b/test/test015/run
@@ -0,0 +1,4 @@
+#!/bin/bash
+idris test015.idr -o test015
+./test015
+rm -f test015 parity.ibc test015.ibc
diff --git a/test/test015/test015.idr b/test/test015/test015.idr
new file mode 100644
index 000000000..5d89b3313
--- /dev/null
+++ b/test/test015/test015.idr
@@ -0,0 +1,141 @@
+module main
+
+import parity
+import system
+
+data Bit : Nat -> Set where
+     b0 : Bit 0
+     b1 : Bit 1
+
+instance Show (Bit n) where
+     show b0 = "0"
+     show b1 = "1"
+
+infixl 5 #
+
+data Binary : (width : Nat) -> (value : Nat) -> Set where
+     zero : Binary O O
+     (#)  : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
+
+instance Show (Binary w k) where
+     show zero = ""
+     show (bin # bit) = show bin ++ show bit
+
+pad : Binary w n -> Binary (S w) n
+pad zero = zero # b0 
+pad (num # x) = pad num # x
+
+natToBin : (width : Nat) -> (n : Nat) ->
+           Maybe (Binary width n)
+natToBin O (S k) = Nothing
+natToBin O O = Just zero
+natToBin (S k) O = do x <- natToBin k O
+                      Just (pad x)
+natToBin (S w) (S k) with (parity k)
+  natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j
+                                            let value = jbin # b1
+                                            ?ntbEven
+  natToBin (S w) (S (S (plus j j))) | odd = do jbin <- natToBin w (S j)
+                                               let value = jbin # b0
+                                               ?ntbOdd
+
+testBin : Maybe (Binary 8 42)
+testBin = natToBin _ _
+
+pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
+term    syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))
+
+addBit : Bit x -> Bit y -> Bit c -> 
+          (bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))
+addBit b0 b0 b0 = bitpair b0 b0
+addBit b0 b0 b1 = bitpair b0 b1 
+addBit b0 b1 b0 = bitpair b0 b1
+addBit b0 b1 b1 = bitpair b1 b0
+addBit b1 b0 b0 = bitpair b0 b1 
+addBit b1 b0 b1 = bitpair b1 b0 
+addBit b1 b1 b0 = bitpair b1 b0 
+addBit b1 b1 b1 = bitpair b1 b1 
+
+adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y) 
+adc zero        zero        carry ?= zero # carry
+adc (numx # bx) (numy # by) carry
+   ?= let (bitpair carry0 lsb) = addBit bx by carry in 
+          adc numx numy carry0 # lsb
+
+readNum : IO Nat
+readNum = do putStr "Enter a number:"
+             i <- getLine
+             let n : Int = cast i
+             return (fromInteger n)
+
+main : IO ()
+main = do let Just bin1 = natToBin 8 42
+          print bin1
+          let Just bin2 = natToBin 8 89
+          print bin2
+          print (adc bin1 bin2 b0)
+
+
+
+
+
+
+    
+---------- Proofs ----------
+
+main.ntbOdd = proof {
+    intro w,j;
+    rewrite sym (plusZeroRightNeutral j);
+    rewrite plusSuccRightSucc j j;
+    intros;
+    refine Just;
+    trivial;
+}
+
+main.ntbEven = proof {
+    compute;
+    intro w,j;
+    rewrite sym (plusZeroRightNeutral j);
+    intros;
+    refine Just;
+    trivial;
+}
+
+-- There is almost certainly an easier proof. I don't care, for now :)
+
+main.adc_lemma_2 = proof {
+    intro c,w,v,bit0,num0;
+    intro b0,v1,bit1,num1,b1;
+    intro bc,x,x1,bx,bx1;
+    rewrite sym (plusZeroRightNeutral x);
+    rewrite sym (plusZeroRightNeutral v1);
+    rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));
+    rewrite sym (plusZeroRightNeutral v);
+    intros;
+    rewrite sym (plusAssociative (plus c (plus bit0 (plus v v))) bit1 (plus v1 v1));
+    rewrite  (plusAssociative c (plus bit0 (plus v v)) bit1);
+    rewrite  (plusAssociative bit0 (plus v v) bit1);
+    rewrite plusCommutative bit1 (plus v v);
+    rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));
+    rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));
+    rewrite sym b;
+    rewrite plusAssociative x1 (plus x x) (plus v v);
+    rewrite plusAssociative x x (plus v v);
+    rewrite sym (plusAssociative x v v);
+    rewrite plusCommutative v (plus x v);
+    rewrite sym (plusAssociative x v (plus x v));
+    rewrite (plusAssociative x1 (plus (plus x v) (plus x v)) (plus v1 v1));
+    rewrite sym (plusAssociative (plus (plus x v) (plus x v)) v1 v1);
+    rewrite  (plusAssociative (plus x v) (plus x v) v1);
+    rewrite (plusCommutative v1 (plus x v));
+    rewrite sym (plusAssociative (plus x v) v1 (plus x v));
+    rewrite (plusAssociative (plus (plus x v) v1) (plus x v) v1);
+    trivial;
+}
+
+main.adc_lemma_1 = proof {
+    intros;
+    rewrite sym (plusZeroRightNeutral c) ;
+    trivial;
+}
+