equal
deleted
inserted
replaced
152 (* name equivalence theorem *) |
152 (* name equivalence theorem *) |
153 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
153 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
154 |
154 |
155 (* storing the quot-info *) |
155 (* storing the quot-info *) |
156 (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *) |
156 (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *) |
157 fun qinfo phi = quotdata_transfer phi |
157 fun qinfo phi = transform_quotdata phi |
158 {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, |
158 {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, |
159 equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm} |
159 equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm} |
160 val lthy4 = Local_Theory.declaration true |
160 val lthy4 = Local_Theory.declaration true |
161 (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 |
161 (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 |
162 in |
162 in |