diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr
index bde7ad9..dc7b990 100644
--- a/src/Core/Binary.idr
+++ b/src/Core/Binary.idr
@@ -139,7 +139,7 @@ readTTCFile modns as r b
            gam' <- updateEntries (gamma defs) modns as 0 (max r) r
            setCtxt gam' 
            holes <- fromBuf r b
-           coreLift $ putStrLn $ "Read " ++ show holes ++ " holes"
+           coreLift $ putStrLn $ "Read " ++ show (length holes) ++ " holes"
            guesses <- fromBuf r b
            coreLift $ putStrLn $ "Read " ++ show (length guesses) ++ " guesses"
            constraints <- the (Core (List (Int, Constraint))) $ fromBuf r b
diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index 3f27203..bc33436 100644
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@@ -420,9 +420,9 @@ TTC GlobalDef where
                  toBuf b (multiplicity gdef)
                  toBuf b (visibility gdef)
                  toBuf b (totality gdef)
+                 toBuf b (flags gdef)
                  toBuf b (map fst (toList (refersTo gdef)))
                  toBuf b (noCycles gdef)
-                 toBuf b (flags gdef)
 
   fromBuf r b 
       = do name <- fromBuf r b
@@ -431,7 +431,8 @@ TTC GlobalDef where
               then do loc <- fromBuf r b; 
                       ty <- fromBuf r b; mul <- fromBuf r b
                       vis <- fromBuf r b; tot <- fromBuf r b
-                      refsList <- fromBuf r b; fl <- fromBuf r b
+                      fl <- fromBuf r b
+                      refsList <- fromBuf r b; 
                       let refs = fromList (map (\x => (x, ())) refsList)
                       c <- fromBuf r b
                       pure (MkGlobalDef loc name ty mul vis tot fl refs c def)
diff --git a/src/Core/Env.idr b/src/Core/Env.idr
index f7f78fa..0862347 100644
--- a/src/Core/Env.idr
+++ b/src/Core/Env.idr
@@ -109,3 +109,9 @@ abstractFullEnvType fc (b :: env) tm
     = abstractFullEnvType fc env (Bind fc _ 
 						(Pi (multiplicity b) Explicit (binderType b)) tm)
 
+export
+letToLam : Env Term vars -> Env Term vars
+letToLam [] = []
+letToLam (Let c val ty :: env) = Lam c Explicit ty :: letToLam env
+letToLam (b :: env) = b :: letToLam env
+
diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr
index 5c5cc08..395ee27 100644
--- a/src/TTImp/Elab/App.idr
+++ b/src/TTImp/Elab/App.idr
@@ -195,8 +195,8 @@ mutual
                   InLHS _ => -- reset hole and redo it with the unexpanded definition
                      do updateDef (Resolved idx) (const (Just (Hole False)))
                         convert fc elabinfo env 
-                                   (gnfOpts withHoles (noLet env) metaval) 
-                                   (gnfOpts withHoles (noLet env) argv)
+                                   (gnfOpts withHoles (letToLam env) metaval) 
+                                   (gnfOpts withHoles (letToLam env) argv)
                         pure ()
                   _ => pure ()
              removeHoleName nm
@@ -216,12 +216,6 @@ mutual
              fnty <- sc defs (toClosure defaultOpts env argv)
              checkAppWith rig elabinfo nest env fc
                           fntm fnty expargs impargs kr expty
-    where
-      noLet : Env Term vs -> Env Term vs
-      noLet [] = []
-      noLet (Let c v t :: env) = Lam c Explicit t :: noLet env
-      noLet (b :: env) = b :: noLet env
-
 
   -- Check an application of 'fntm', with type 'fnty' to the given list
   -- of explicit and implicit arguments.
diff --git a/src/TTImp/Elab/Hole.idr b/src/TTImp/Elab/Hole.idr
new file mode 100644
index 0000000..12e95e5
--- /dev/null
+++ b/src/TTImp/Elab/Hole.idr
@@ -0,0 +1,38 @@
+module TTImp.Elab.As
+
+import Core.Context
+import Core.Core
+import Core.Env
+import Core.Normalise
+import Core.Unify
+import Core.TT
+import Core.Value
+
+import TTImp.Elab.Check
+import TTImp.TTImp
+
+%default covering
+
+export
+checkHole : {vars : _} ->
+            {auto c : Ref Ctxt Defs} ->
+            {auto u : Ref UST UState} ->
+            {auto e : Ref EST (EState vars)} ->
+            RigCount -> ElabInfo ->
+            NestedNames vars -> Env Term vars -> 
+            FC -> String -> Maybe (Glued vars) ->
+            Core (Term vars, Glued vars)
+checkHole rig elabinfo nest env fc n_in (Just gexpty)
+    = do nm <- inCurrentNS (UN n_in)
+         expty <- getTerm gexpty
+         let env' = letToLam env -- we want all the names to appear in the
+                                 -- hole type
+         metaval <- metaVar fc rig env' nm expty
+         pure (metaval, gexpty)
+checkHole rig elabinfo nest env fc n_in exp
+    = do nmty <- genName "holeTy"
+         ty <- metaVar fc Rig0 env nmty (TType fc)
+         nm <- inCurrentNS (UN n_in)
+         let env' = letToLam env
+         metaval <- metaVar fc rig env' nm ty
+         pure (metaval, gnf env ty)
diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr
index 8a4f0b6..d9fc30f 100644
--- a/src/TTImp/Elab/Term.idr
+++ b/src/TTImp/Elab/Term.idr
@@ -14,6 +14,7 @@ import TTImp.Elab.As
 import TTImp.Elab.Binders
 import TTImp.Elab.Case
 import TTImp.Elab.Check
+import TTImp.Elab.Hole
 import TTImp.Elab.ImplicitBind
 import TTImp.Elab.Local
 import TTImp.Elab.Prim
@@ -142,7 +143,7 @@ checkTerm rig elabinfo nest env (IType fc) exp
     = checkExp rig elabinfo env fc (TType fc) (gType fc) exp
 
 checkTerm rig elabinfo nest env (IHole fc str) exp
-    = throw (InternalError "holes not implemented")
+    = checkHole rig elabinfo nest env fc str exp
 checkTerm rig elabinfo nest env (Implicit fc b) (Just gexpty)
     = do nm <- genName "imp"
          expty <- getTerm gexpty
diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr
index e15eb54..0f3d070 100644
--- a/src/TTImp/Parser.idr
+++ b/src/TTImp/Parser.idr
@@ -45,6 +45,10 @@ atom fname
          x <- unqualifiedName
          end <- location
          pure (IBindVar (MkFC fname start end) x)
+  <|> do start <- location
+         x <- holeName
+         end <- location
+         pure (IHole (MkFC fname start end) x)
 
 visibility : EmptyRule Visibility
 visibility
diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr
index 84c4827..19a7d02 100644
--- a/src/TTImp/ProcessDef.idr
+++ b/src/TTImp/ProcessDef.idr
@@ -154,7 +154,7 @@ checkClause mult hashit n nest env (PatClause fc lhs_in rhs)
          -- Normalise the LHS to get any functions or let bindings evaluated
          -- (this might be allowed, e.g. for 'fromInteger')
          defs <- get Ctxt
-         lhstm <- normaliseLHS defs (noLet env) lhstm
+         lhstm <- normaliseLHS defs (letToLam env) lhstm
          lhsty <- normaliseHoles defs env lhsty
          linvars_in <- findLinear True 0 Rig1 lhstm
          log 5 $ "Linearity of names in " ++ show n ++ ": " ++ 
@@ -174,11 +174,6 @@ checkClause mult hashit n nest env (PatClause fc lhs_in rhs)
 
          logTerm 5 "RHS term" rhstm
          pure (Just (MkClause env' lhstm' rhstm))
-  where
-    noLet : Env Term vs -> Env Term vs
-    noLet [] = []
-    noLet (Let c v t :: env) = Lam c Explicit t :: noLet env
-    noLet (b :: env) = b :: noLet env
 
 toPats : Clause -> (vs ** (Env Term vs, Term vs, Term vs))
 toPats (MkClause {vars} env lhs rhs) 
diff --git a/tests/Main.idr b/tests/Main.idr
index 2a66dfb..625517c 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -7,7 +7,7 @@ import System
 ttimpTests : List String
 ttimpTests 
     = ["basic001", "basic002", "basic003", "basic004", "basic005",
-       "basic006",
+       "basic006", "basic007",
        "eta001", "eta002",
        "nest001", "nest002",
        "perf001", "perf002", "perf003"]
diff --git a/tests/ttimp/basic001/expected b/tests/ttimp/basic001/expected
index ed33576..62eb8a0 100644
--- a/tests/ttimp/basic001/expected
+++ b/tests/ttimp/basic001/expected
@@ -4,7 +4,7 @@ Yaffle> (Main.S (Main.S (Main.S (Main.S Main.Z))))
 Yaffle> (Main.S (Main.S (Main.S (Main.S (Main.S Main.Z)))))
 Yaffle> Bye for now!
 Processing as TTC
-Read [] holes
+Read 0 holes
 Read 0 guesses
 Read 31 constraints
 Read TTC
diff --git a/tests/ttimp/basic007/Hole.yaff b/tests/ttimp/basic007/Hole.yaff
new file mode 100644
index 0000000..d5e06bd
--- /dev/null
+++ b/tests/ttimp/basic007/Hole.yaff
@@ -0,0 +1,15 @@
+data Nat : Type where
+     Z : Nat
+     S : Nat -> Nat
+
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z $a
+     Cons : $a -> Vect $k $a -> Vect (S $k) $a
+
+plus : Nat -> Nat -> Nat
+plus Z $y = y
+plus (S $k) $y = S (plus k y)
+
+append : Vect $n $a -> Vect $m $a -> Vect (plus $n $m) $a
+append Nil $ys = ys
+append (Cons $x $xs) $ys = Cons $x ?foo
diff --git a/tests/ttimp/basic007/expected b/tests/ttimp/basic007/expected
new file mode 100644
index 0000000..994ad84
--- /dev/null
+++ b/tests/ttimp/basic007/expected
@@ -0,0 +1,11 @@
+Processing as TTImp
+Written TTC
+Yaffle> (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
+Yaffle> Bye for now!
+Processing as TTC
+Read 2 holes
+Read 0 guesses
+Read 0 constraints
+Read TTC
+Yaffle> (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
+Yaffle> Bye for now!
diff --git a/tests/ttimp/basic007/input b/tests/ttimp/basic007/input
new file mode 100644
index 0000000..6b0118e
--- /dev/null
+++ b/tests/ttimp/basic007/input
@@ -0,0 +1,2 @@
+:t foo
+:q
diff --git a/tests/ttimp/basic007/run b/tests/ttimp/basic007/run
new file mode 100755
index 0000000..641d174
--- /dev/null
+++ b/tests/ttimp/basic007/run
@@ -0,0 +1,4 @@
+$1 Hole.yaff < input
+$1 build/Hole.ttc < input
+
+rm -rf build
diff --git a/yaffle.ipkg b/yaffle.ipkg
index cb32772..42dd2b7 100644
--- a/yaffle.ipkg
+++ b/yaffle.ipkg
@@ -45,6 +45,7 @@ modules =
     TTImp.Elab.As,
     TTImp.Elab.Binders,
     TTImp.Elab.Check,
+    TTImp.Elab.Hole,
     TTImp.Elab.ImplicitBind,
     TTImp.Elab.Local,
     TTImp.Elab.Prim,