equal
deleted
inserted
replaced
258 ML {* |
258 ML {* |
259 fun lookup_quot_data lthy qty = |
259 fun lookup_quot_data lthy qty = |
260 let |
260 let |
261 val qty_name = fst (dest_Type qty) |
261 val qty_name = fst (dest_Type qty) |
262 val SOME quotdata = quotdata_lookup lthy qty_name |
262 val SOME quotdata = quotdata_lookup lthy qty_name |
263 (* cu: Changed the lookup\<dots>not sure whether this works *) |
|
264 (* TODO: Should no longer be needed *) |
263 (* TODO: Should no longer be needed *) |
265 val rty = Logic.unvarifyT (#rtyp quotdata) |
264 val rty = Logic.unvarifyT (#rtyp quotdata) |
266 val rel = #rel quotdata |
265 val rel = #rel quotdata |
267 val rel_eqv = #equiv_thm quotdata |
266 val rel_eqv = #equiv_thm quotdata |
268 val rel_refl = @{thm equivp_reflp} OF [rel_eqv] |
267 val rel_refl = @{thm equivp_reflp} OF [rel_eqv] |