equal
deleted
inserted
replaced
115 val var_strs = map (Syntax.string_of_term lthy) vars; |
115 val var_strs = map (Syntax.string_of_term lthy) vars; |
116 fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = |
116 fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = |
117 if is_atom tyS then HOLogic.mk_set ty [t] else |
117 if is_atom tyS then HOLogic.mk_set ty [t] else |
118 if (Long_Name.base_name tyS) mem dt_names then |
118 if (Long_Name.base_name tyS) mem dt_names then |
119 Free ("fv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t else |
119 Free ("fv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t else |
120 @{term "{}"} |
120 HOLogic.mk_set @{typ name} [] |
121 val fv_eq = |
121 val fv_eq = |
122 if null vars then HOLogic.mk_set @{typ atom} [] |
122 if null vars then HOLogic.mk_set @{typ name} [] |
123 else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) |
123 else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) |
124 val fv_eq_str = Syntax.string_of_term lthy fv_eq |
124 val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq) |
125 in |
125 in |
126 prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str |
126 prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str |
127 end |
127 end |
128 *} |
128 *} |
129 |
129 |