@@ -1899,31 +1899,35 @@ allNamesIn tm = nub $ ni [] tm
1899 niTacImp env (TacImp _ _ scr) = ni env scr
1899 niTacImp env (TacImp _ _ scr) = ni env scr
1900 niTacImp _ _ = []
1900 niTacImp _ _ = []
1902-- Return all names defined in binders in the given term
1903-- Return all names defined in binders in the given term
1903boundNamesIn :: PTerm -> [Name]
1904boundNamesIn :: PTerm -> [Name]
1904−boundNamesIn tm = nub $ ni tm
1905+boundNamesIn tm = S.toList (ni S.empty tm)
1905 where -- TODO THINK Added niTacImp, but is it right?
1906 where -- TODO THINK Added niTacImp, but is it right?
1906− ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1907+ ni set (PApp _ f as) = niTms (ni set f) (map getTm as)
1907− ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1908+ ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
1908− ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1909+ ni set (PCase _ c os) = niTms (ni set c) (map snd os)
1909− ni (PLam fc n ty sc) = n : (ni ty ++ ni sc)
1910+ ni set (PLam fc n ty sc) = S.insert n $ ni (ni set ty) sc
1910− ni (PLet fc n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1911+ ni set (PLet fc n ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
1911− ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1912+ ni set (PPi p n ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
1912− ni (PEq _ _ _ l r) = ni l ++ ni r
1913+ ni set (PEq _ _ _ l r) = ni (ni set l) r
1913− ni (PRewrite _ l r _) = ni l ++ ni r
1914+ ni set (PRewrite _ l r _) = ni (ni set l) r
1914− ni (PTyped l r) = ni l ++ ni r
1915+ ni set (PTyped l r) = ni (ni set l) r
1915− ni (PPair _ _ l r) = ni l ++ ni r
1916+ ni set (PPair _ _ l r) = ni (ni set l) r
1916− ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1917+ ni set (PDPair _ _ (PRef _ n) t r) = ni (ni set t) r
1917− ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1918+ ni set (PDPair _ _ l t r) = ni (ni (ni set l) t) r
1918− ni (PAlternative a as) = concatMap (ni) as
1919+ ni set (PAlternative a as) = niTms set as
1919− ni (PHidden tm) = ni tm
1920+ ni set (PHidden tm) = ni set tm
1920− ni (PUnifyLog tm) = ni tm
1921+ ni set (PUnifyLog tm) = ni set tm
1921− ni (PDisamb _ tm) = ni tm
1922+ ni set (PDisamb _ tm) = ni set tm
1922− ni (PNoImplicits tm) = ni tm
1923+ ni set (PNoImplicits tm) = ni set tm
1923− ni _ = []
1924+ ni set _ = set
1927+ niTms set (x : xs) = niTms (ni set x) xs
1925− niTacImp (TacImp _ _ scr) = ni scr
1929+ niTacImp set (TacImp _ _ scr) = ni set scr
1926− niTacImp _ = []
1930+ niTacImp set _ = set
1928-- Return names which are valid implicits in the given term (type).
1932-- Return names which are valid implicits in the given term (type).
1929implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1933implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]