src/pattern_matches/patternMatchesLib.sml

405      val avoid = free_vars p1
408        ((v |-> v')::s, v'::av) end) ([], avoid) (free_vars p2)
1046      val avoid = free_varsl [pt, gt, rh]
1058              if (List.null vars') then [variant avoid ``_uv:unit``] else vars'
1077            val vars' = if (List.null vars') then [variant avoid ``_uv:unit``] else vars'
1189     fun ff_inv_var avoid tt = let
1196       val gen_fun = mk_var_gen (var_basename ^ "_") avoid;
1257      val avoid = vars @ free_vars pt @ free_vars rh @ free_vars gt
1258      val (pt', pv, new_vars) = ff_inv_var avoid pt
1265        if (List.null vars') then [variant avoid ``_uv:unit``] else vars'
1423     val avoid = all_varsl [t, nv]
1424     val gen_fun = mk_var_gen "_" avoid
1572   fun split_var avoid cols l = let
1583     val gen_fun = mk_var_gen (var_basename ^ "_") avoid;
1722 fun force_unique_vars s no_change avoid t =
1725       if (mem t no_change) then (s, avoid, t) else
1727          val v' = variant avoid t
1728          val avoid' = v'::avoid
1730       in (s', avoid', v') end
1731     | Psyntax.CONST _ => (s, avoid, t)
1733          val (s', avoid', t'') = force_unique_vars s (v::no_change)
1734            (v::avoid) t'
1736          (s', avoid', mk_abs (v, t''))
1739          val (s', avoid', t1') = force_unique_vars s no_change avoid t1
1740          val (s'', avoid'', t2') = force_unique_vars s' no_change avoid' t2
1742          (s'', avoid'', mk_comb (t1', t2'))
2142   fun mk_pair avoid acc col_no v = if (col_no <= 1) then (
2152          val v1 = variant avoid (mk_var ("v", ty1))
2153          val v2 = variant (v1::avoid) (mk_var ("v", ty2))
2157          val t2a = mk_pair (v1::v2::avoid) (v1::acc) (col_no-1) v2
3311 fun rename_uscore_vars ren avoid [] = ren
3312   | rename_uscore_vars ren avoid (v::vs) =
3316       val v' = variant avoid (mk_var ("v", v_ty))
3318       rename_uscore_vars ((v |-> v')::ren) (v'::avoid) vs
3319     end handle HOL_ERR _ => rename_uscore_vars ren avoid vs
3393         val avoid = free_vars row @ to_ren
3394         val ren = rename_uscore_vars [] avoid to_ren