Lines Matching defs:avoid
539 fun subst_rename (v,(avoid,bv,sub,domain,fvSub)) =
541 val v' = Term.variantPrime avoid v
542 val avoid = NameSet.add avoid v'
548 (avoid,bv,sub,domain,fvSub)
585 val avoid = NameSet.union fv bv
587 NameSet.foldl subst_rename (avoid,bv,sub,domain,fvSub) captured
716 fun rename avoid fv bv fm =
718 val captured = NameSet.intersect avoid bv
730 val avoid = NameSet.union (NameSet.union avoid fv) bv
732 val (_,sub) = NameSet.foldl ren (avoid,Subst.empty) captured
738 fun cnfFm avoid fm =
741 val fm' = cnfFm' avoid fm
747 and cnfFm' avoid fm =
753 | And (_,_,s) => AndList (Set.transform (cnfFm avoid) s)
756 val avoid = NameSet.union avoid fv
757 val (fms,_) = Set.foldl cnfOr ([],avoid) s
761 | Xor _ => cnfFm avoid (pushXor fm)
762 | Exists (fv,_,n,f) => cnfFm avoid (skolemize fv n f)
763 | Forall (fv,_,n,f) => cnfFm avoid (rename avoid fv n f)
765 and cnfOr (fm,(fms,avoid)) =
767 val fm = cnfFm avoid fm
769 val avoid = NameSet.union avoid (freeVars fm)
771 (fms,avoid)