@@ -474,6 +474,7 @@ elab ist info emode opts fn tm
474474 guarded = e_guarded ec
475475 inty = e_intype ec
476476 ctxt <- get_context
477+
477478 let defined = case lookupTy n ctxt of
478479 [] -> False
479480 _ -> True
@@ -485,7 +486,10 @@ elab ist info emode opts fn tm
485486 update_term liftPats
486487 highlightSource fc (AnnBoundName n False)
487488 else if (defined && not guarded)
488− then do apply (Var n) []; solve
489+ then do apply (Var n) []
490+ annot <- findHighlight n
491+ solve
492+ highlightSource fc annot
489493 else try (do apply (Var n) []
490494 annot <- findHighlight n
491495 solve
@@ -693,7 +697,7 @@ elab ist info emode opts fn tm
693697 if (f `elem` map fst env && length args == 1 && length args_in == 1)
694698 then -- simple app, as below
695699 do simple_app False
696− (elabE (ina { e_isfn = True }) (Just fc) (PRef fc f))
700+ (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc f))
697701 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
698702 (show tm)
699703 solve