equal
deleted
inserted
replaced
1030 ML {* |
1030 ML {* |
1031 fun lookup_quot_data lthy qty = |
1031 fun lookup_quot_data lthy qty = |
1032 let |
1032 let |
1033 fun matches (ty1, ty2) = |
1033 fun matches (ty1, ty2) = |
1034 Type.raw_instance (ty1, Logic.varifyT ty2); |
1034 Type.raw_instance (ty1, Logic.varifyT ty2); |
1035 val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) |
1035 val qty_name = fst (dest_Type qty) |
|
1036 val SOME quotdata = quotdata_lookup lthy qty_name |
|
1037 (* cu: Changed the lookup\<dots>not sure whether this works *) |
1036 (* TODO: Should no longer be needed *) |
1038 (* TODO: Should no longer be needed *) |
1037 val rty = Logic.unvarifyT (#rtyp quotdata) |
1039 val rty = Logic.unvarifyT (#rtyp quotdata) |
1038 val rel = #rel quotdata |
1040 val rel = #rel quotdata |
1039 val rel_eqv = #equiv_thm quotdata |
1041 val rel_eqv = #equiv_thm quotdata |
1040 val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv] |
1042 val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv] |