Lines Matching defs:domain
539 fun subst_rename (v,(avoid,bv,sub,domain,fvSub)) =
545 val domain = NameSet.add domain v
548 (avoid,bv,sub,domain,fvSub)
551 fun subst_check sub domain fvSub fm =
553 val domain = NameSet.intersect domain (freeVars fm)
555 if NameSet.null domain then fm
556 else subst_domain sub domain fvSub fm
559 and subst_domain sub domain fvSub fm =
563 val fv = NameSet.difference fv domain
564 val fv = NameSet.union fv (subst_fv fvSub domain)
570 AndList (Set.transform (subst_check sub domain fvSub) s)
572 OrList (Set.transform (subst_check sub domain fvSub) s)
574 XorPolarityList (p, Set.transform (subst_check sub domain fvSub) s)
575 | Exists fv_c_n_f => subst_quant Exists sub domain fvSub fv_c_n_f
576 | Forall fv_c_n_f => subst_quant Forall sub domain fvSub fv_c_n_f
579 and subst_quant quant sub domain fvSub (fv,c,bv,fm) =
581 val sub_fv = subst_fv fvSub domain
582 val fv = NameSet.union sub_fv (NameSet.difference fv domain)
586 val (_,bv,sub,domain,fvSub) =
587 NameSet.foldl subst_rename (avoid,bv,sub,domain,fvSub) captured
588 val fm = subst_domain sub domain fvSub fm
599 val (domain,fvSub) = Subst.foldl mk_dom domain_fvSub sub
601 subst_check sub domain fvSub