Nominal/NewFv.thy
changeset 2131 f7ec6f7b152e
parent 2071 843e0a2d44d7
child 2133 16834a4ca1bb
equal deleted inserted replaced
2130:5111dadd1162 2131:f7ec6f7b152e
   131 
   131 
   132 ML {*
   132 ML {*
   133 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
   133 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
   134 let
   134 let
   135   val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys)
   135   val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys)
   136   val bound_vars =
   136   fun bound_var (SOME bn, i) = set (bn $ nth args i)
   137     case binds of
   137     | bound_var (NONE, i) = fv_body thy dts args fv_frees false i
   138       [(SOME bn, i)] => set (bn $ nth args i)
   138   val bound_vars = mk_union (map bound_var binds);
   139     | _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds));
       
   140   val non_rec_vars =
   139   val non_rec_vars =
   141     case binds of
   140     case binds of
   142       [(SOME bn, i)] =>
   141       [(SOME bn, i)] =>
   143         if member (op =) bodys i
   142         if member (op =) bodys i
   144         then noatoms
   143         then noatoms