equal
deleted
inserted
replaced
108 fun fv_bds s bds set = |
108 fun fv_bds s bds set = |
109 case bds of |
109 case bds of |
110 [] => set |
110 [] => set |
111 | B (s1, s2) :: tl => |
111 | B (s1, s2) :: tl => |
112 if s2 = s then |
112 if s2 = s then |
113 fv_bds s tl (HOLogic.mk_binop @{const_name "HOL.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) |
113 fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) |
114 else fv_bds s tl set |
114 else fv_bds s tl set |
115 | BS (s1, s2) :: tl => |
115 | BS (s1, s2) :: tl => |
116 (* TODO: This is just a copy *) |
116 (* TODO: This is just a copy *) |
117 if s2 = s then |
117 if s2 = s then |
118 fv_bds s tl (HOLogic.mk_binop @{const_name "HOL.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) |
118 fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) |
119 else fv_bds s tl set |
119 else fv_bds s tl set |
120 *} |
120 *} |
121 |
121 |
122 (* TODO: After variant_frees, check that the new names correspond to the ones given by user |
122 (* TODO: After variant_frees, check that the new names correspond to the ones given by user |
123 so that 'bind' is matched with variables correctly *) |
123 so that 'bind' is matched with variables correctly *) |