equal
deleted
inserted
replaced
157 | _ => raise EQVT_FORM "Type unknown") |
157 | _ => raise EQVT_FORM "Type unknown") |
158 in |
158 in |
159 fold (fn thm => Data.map (flag thm)) thms_to_be_added context |
159 fold (fn thm => Data.map (flag thm)) thms_to_be_added context |
160 end |
160 end |
161 handle EQVT_FORM s => |
161 handle EQVT_FORM s => |
162 error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").") |
162 error (Display.string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").") |
163 |
163 |
164 (* in cases of bij- and freshness, we just add the lemmas to the *) |
164 (* in cases of bij- and freshness, we just add the lemmas to the *) |
165 (* data-slot *) |
165 (* data-slot *) |
166 |
166 |
167 fun eqvt_map f (r:Data.T) = {eqvts = f (#eqvts r), freshs = #freshs r, bijs = #bijs r}; |
167 fun eqvt_map f (r:Data.T) = {eqvts = f (#eqvts r), freshs = #freshs r, bijs = #bijs r}; |