62 ML {* |
62 ML {* |
63 fun atoms thy t = |
63 fun atoms thy t = |
64 let |
64 let |
65 val ty = fastype_of t; |
65 val ty = fastype_of t; |
66 in |
66 in |
67 if is_atom thy ty |
67 if is_atom thy ty |
68 then mk_singleton_atom t |
68 then mk_singleton_atom t |
69 else if is_atom_set thy ty |
69 else if is_atom_set thy ty |
70 then mk_atom_set t |
70 then mk_atom_set t |
71 else if is_atom_fset thy ty |
71 else if is_atom_fset thy ty |
72 then mk_atom_fset t |
72 then mk_atom_fset t |
73 else noatoms |
73 else noatoms |
74 end |
74 end |
75 *} |
75 *} |
76 |
76 |
77 ML {* |
77 ML {* |
78 fun mk_supp t = |
|
79 Const (@{const_name supp}, fastype_of t --> @{typ "atom set"}) $ t |
|
80 *} |
|
81 |
|
82 ML {* |
|
83 fun setify x = |
78 fun setify x = |
84 if fastype_of x = @{typ "atom list"} |
79 if fastype_of x = @{typ "atom list"} |
85 then @{term "set::atom list \<Rightarrow> atom set"} $ x |
80 then @{term "set::atom list \<Rightarrow> atom set"} $ x |
86 else x |
81 else x |
87 *} |
82 *} |
88 |
83 |
89 ML {* |
84 ML {* |
90 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = |
85 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = |
91 let |
86 let |
92 fun fv_body i = |
87 fun fv_body supp i = |
93 let |
88 let |
94 val x = nth args i; |
89 val x = nth args i; |
95 val dt = nth dts i; |
90 val dt = nth dts i; |
96 in |
91 in |
97 if Datatype_Aux.is_rec_type dt |
92 if Datatype_Aux.is_rec_type dt |
98 then nth fv_frees (Datatype_Aux.body_index dt) $ x |
93 then nth fv_frees (Datatype_Aux.body_index dt) $ x |
99 else mk_supp x |
94 else (if supp then mk_supp x else atoms thy x) |
100 end |
95 end |
101 val fv_bodys = mk_union (map fv_body bodys) |
96 val fv_bodys = mk_union (map (fv_body true) bodys) |
102 val bound_vars = |
97 val bound_vars = |
103 case binds of |
98 case binds of |
104 [(SOME bn, i)] => setify (bn $ nth args i) |
99 [(SOME bn, i)] => setify (bn $ nth args i) |
105 | _ => mk_union (map fv_body (map snd binds)); |
100 | _ => mk_union (map (fv_body false) (map snd binds)); |
106 val non_rec_vars = |
101 val non_rec_vars = |
107 case binds of |
102 case binds of |
108 [(SOME bn, i)] => |
103 [(SOME bn, i)] => |
109 if i mem bodys |
104 if i mem bodys |
110 then ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i) |
105 then ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i) |