Nominal/NewFv.thy
changeset 1985 727e0edad284
parent 1984 92f40c13d581
child 1986 522748f37444
equal deleted inserted replaced
1984:92f40c13d581 1985:727e0edad284
   100     | _ => mk_union (map (fv_body false) (map snd binds));
   100     | _ => mk_union (map (fv_body false) (map snd binds));
   101   val non_rec_vars =
   101   val non_rec_vars =
   102     case binds of
   102     case binds of
   103       [(SOME bn, i)] =>
   103       [(SOME bn, i)] =>
   104         if i mem bodys
   104         if i mem bodys
   105         then ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
   105         then noatoms
   106         else noatoms
   106         else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
   107     | _ => noatoms
   107     | _ => noatoms
   108 in
   108 in
   109   mk_union [mk_diff fv_bodys bound_vars, non_rec_vars]
   109   mk_union [mk_diff fv_bodys bound_vars, non_rec_vars]
   110 end
   110 end
   111 *}
   111 *}