Lines Matching refs:ren
146 fun ren _ [tm] [] = tm
147 | ren avoid (b :: a :: dealt) (INL NONE :: rest) =
148 ren avoid (mk_comb (a, b) :: dealt) rest
149 | ren avoid (b :: dealt) (INL (SOME v) :: rest) =
150 ren avoid (mk_abs (v, b) :: dealt) rest
151 | ren avoid dealt (INR (sub, tm) :: rest) =
153 CONST _ => ren avoid (tm :: dealt) rest
154 | VAR _ => ren avoid (subst sub tm :: dealt) rest
156 ren avoid dealt (INR (sub, a) :: INR (sub, b) :: INL NONE :: rest)
165 ren (insert v' avoid) dealt (INR (sub', b) :: INL (SOME v') :: rest)
167 | ren _ _ _ = raise ERR "prettify_vars" "BUG";
169 fun prettify_vars tm = ren (all_vars tm) [] [INR ([], tm)];