@@ -474,6 +474,7 @@ elab ist info emode opts fn tm
474 guarded = e_guarded ec
474 guarded = e_guarded ec
475 inty = e_intype ec
475 inty = e_intype ec
476 ctxt <- get_context
476 ctxt <- get_context
477 let defined = case lookupTy n ctxt of
478 let defined = case lookupTy n ctxt of
478 [] -> False
479 [] -> False
479 _ -> True
480 _ -> True
@@ -485,7 +486,10 @@ elab ist info emode opts fn tm
485 update_term liftPats
486 update_term liftPats
486 highlightSource fc (AnnBoundName n False)
487 highlightSource fc (AnnBoundName n False)
487 else if (defined && not guarded)
488 else if (defined && not guarded)
488− then do apply (Var n) []; solve
489+ then do apply (Var n) []
490+ annot <- findHighlight n
492+ highlightSource fc annot
489 else try (do apply (Var n) []
493 else try (do apply (Var n) []
490 annot <- findHighlight n
494 annot <- findHighlight n
@@ -693,7 +697,7 @@ elab ist info emode opts fn tm
693 if (f `elem` map fst env && length args == 1 && length args_in == 1)
697 if (f `elem` map fst env && length args == 1 && length args_in == 1)
694 then -- simple app, as below
698 then -- simple app, as below
695 do simple_app False
699 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))
697 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
701 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
698 (show tm)
702 (show tm)