diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 3215f00ea..befe0ce3f 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -1776,7 +1776,7 @@ parserCommandsForHelp : CommandTable
 parserCommandsForHelp =
   [ exprArgCmd (ParseREPLCmd ["t", "type"]) Check "Check the type of an expression"
   , nameArgCmd (ParseREPLCmd ["printdef"]) PrintDef "Show the definition of a function"
-  , nameArgCmd (ParseREPLCmd ["s", "search"]) ProofSearch "Search for values by type"
+  , exprArgCmd (ParseREPLCmd ["s", "search"]) ProofSearch "Search for values by type"
   , nameArgCmd (ParseIdentCmd "di") DebugInfo "Show debugging information for a name"
   , moduleArgCmd (ParseKeywordCmd "module") ImportMod "Import an extra module"
   , noArgCmd (ParseREPLCmd ["q", "quit", "exit"]) Quit "Exit the Idris system"
diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
index 6ae9bde1c..99bcc8be3 100644
--- a/src/Idris/REPL.idr
+++ b/src/Idris/REPL.idr
@@ -712,14 +712,37 @@ process (Exec ctm)
     = execExp ctm
 process Help
     = pure RequestedHelp
-process (ProofSearch n_in)
-    = do defs <- get Ctxt
-         [(n, i, ty)] <- lookupTyName n_in (gamma defs)
-              | [] => throw (UndefinedName replFC n_in)
-              | ns => throw (AmbiguousName replFC (map fst ns))
-         tm <- search replFC top False 1000 n ty []
-         itm <- resugar [] !(normaliseHoles defs [] tm)
-         pure $ ProofFound itm
+process (ProofSearch (PType fc))
+    = do let ty = gType fc
+         logGlue "repl.ps" 2 "tst" [] ty
+         pure Done
+process (ProofSearch pterm)
+    = do ttimp <- desugar AnyExpr [] pterm 
+         logRaw "repl.ps" 2 "tst" ttimp
+         log "repl.ps" 2 (show (getFn ttimp))
+         let ty = gType (getFC ttimp)
+         logGlue "repl.ps" 2 "gType" [] ty
+         let n = (UN "[input]")
+         inidx <- resolveName n 
+         -- (tm1, gl1) <- check top (initElabInfo InType) (MkNested []) [] ttimp Nothing
+         -- logTermNF "repl.ps" 2 "tst" [] tm1
+         -- logGlue "repl.ps" 2 "tst" [] gl1
+         (tm, gl) <- elabTerm inidx InType [] (MkNested [])
+                                  [] ttimp Nothing
+         logTermNF "repl.ps" 2 "tst" [] tm
+         logGlue "repl.ps" 2 "tst" [] gl
+
+         addNameType replFC n [] tm
+         searchResults <- exprSearchN replFC 3 n []
+         pure $ log $ show searchResults
+
+         tm' <- search replFC top False 1000 n tm []
+         defs <- get Ctxt
+         fnms <- toFullNames !(normaliseAll defs [] tm')
+         itm <- resugar [] fnms
+         logTermNF "repl.ps" 2 "tst" [] fnms
+         pure $ ProofFound $ itm
+
 process (Missing n)
     = do defs <- get Ctxt
          case !(lookupCtxtName n (gamma defs)) of
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index 95980c98c..476c051dc 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -422,7 +422,7 @@ data REPLCmd : Type where
      Compile : PTerm -> String -> REPLCmd
      Exec : PTerm -> REPLCmd
      Help : REPLCmd
-     ProofSearch : Name -> REPLCmd
+     ProofSearch : PTerm -> REPLCmd
      DebugInfo : Name -> REPLCmd
      SetOpt : REPLOpt -> REPLCmd
      GetOpts : REPLCmd