equal
deleted
inserted
replaced
129 val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); |
129 val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); |
130 val var_strs = map (Syntax.string_of_term lthy) vars; |
130 val var_strs = map (Syntax.string_of_term lthy) vars; |
131 fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = |
131 fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = |
132 if is_atom tyS then HOLogic.mk_set ty [t] else |
132 if is_atom tyS then HOLogic.mk_set ty [t] else |
133 if (Long_Name.base_name tyS) mem dt_names then |
133 if (Long_Name.base_name tyS) mem dt_names then |
134 fv_bds s bds (Free ("fv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else |
134 fv_bds s bds (Free ("rfv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else |
135 HOLogic.mk_set @{typ name} [] |
135 HOLogic.mk_set @{typ name} [] |
136 val fv_eq = |
136 val fv_eq = |
137 if null vars then HOLogic.mk_set @{typ name} [] |
137 if null vars then HOLogic.mk_set @{typ name} [] |
138 else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) |
138 else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) |
139 val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq) |
139 val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq) |
153 |> implode |
153 |> implode |
154 *} |
154 *} |
155 |
155 |
156 ML {* |
156 ML {* |
157 fun fv_dt lthy dt_names (((s2, s3), syn), constrs) = |
157 fun fv_dt lthy dt_names (((s2, s3), syn), constrs) = |
158 map (fv_constr lthy ("fv_" ^ Binding.name_of s3) dt_names) constrs |
158 map (fv_constr lthy ("rfv_" ^ Binding.name_of s3) dt_names) constrs |
159 |> separate "\n" |
159 |> separate "\n" |
160 |> implode |
160 |> implode |
161 *} |
161 *} |
162 |
162 |
163 ML {* fun single_fun_eq lthy (at, s) = |
163 ML {* fun single_fun_eq lthy (at, s) = |