@@ -1058,7 +1058,8 @@ implicitise syn ist tm
1058addImpl :: IState -> PTerm -> PTerm
1058addImpl :: IState -> PTerm -> PTerm
1059addImpl ist ptm = ai [] ptm
1059addImpl ist ptm = ai [] ptm
1061− ai env (PRef fc f) = aiFn ist fc f []
1061+ ai env (PRef fc f)
1062+ | not (f `elem` env) = aiFn ist fc f []
1062 ai env (PEq fc l r) = let l' = ai env l
1063 ai env (PEq fc l r) = let l' = ai env l
1063 r' = ai env r in
1064 r' = ai env r in
1064 PEq fc l' r'
1065 PEq fc l' r'
@@ -1072,6 +1073,7 @@ addImpl ist ptm = ai [] ptm
1072 ai env (PAlternative as) = let as' = map (ai env) as in
1073 ai env (PAlternative as) = let as' = map (ai env) as in
1073 PAlternative as'
1074 PAlternative as'
1074 ai env (PApp fc (PRef _ f) as)
1075 ai env (PApp fc (PRef _ f) as)
1076+ | not (f `elem` env)
1075 = let as' = map (fmap (ai env)) as in
1077 = let as' = map (fmap (ai env)) as in
1076 aiFn ist fc f as'
1078 aiFn ist fc f as'
1077 ai env (PApp fc f as) = let f' = ai env f
1079 ai env (PApp fc f as) = let f' = ai env f