Lines Matching defs:avoid
22 fun mk_var_gen prefix avoid = let
24 val avoidL = List.map (fst o dest_var) avoid
36 fun mk_wildcard_gen avoid = mk_var_gen "_" avoid
224 fun REMOVE_REBIND_CONV_AUX avoid t = let
226 val v' = variant avoid v
228 val (t''', avoid') = REMOVE_REBIND_CONV_AUX (v'::avoid) t''
230 (mk_abs (v', t'''), avoid')
233 val (t1', avoid1) = REMOVE_REBIND_CONV_AUX avoid t1
237 end handle HOL_ERR _ => (t, avoid)
306 val avoid = HOLset.listItems (HOLset.union (grd_s, p_s))
307 val mk_wc = mk_wildcard_gen avoid
308 val mk_var = mk_var_gen "v" avoid