@@ -1058,7 +1058,8 @@ implicitise syn ist tm
10581058addImpl :: IState -> PTerm -> PTerm
10591059addImpl ist ptm = ai [] ptm
10601060 where
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 []
10621063 ai env (PEq fc l r) = let l' = ai env l
10631064 r' = ai env r in
10641065 PEq fc l' r'
@@ -1072,6 +1073,7 @@ addImpl ist ptm = ai [] ptm
10721073 ai env (PAlternative as) = let as' = map (ai env) as in
10731074 PAlternative as'
10741075 ai env (PApp fc (PRef _ f) as)
1076+ | not (f `elem` env)
10751077 = let as' = map (fmap (ai env)) as in
10761078 aiFn ist fc f as'
10771079 ai env (PApp fc f as) = let f' = ai env f