equal
deleted
inserted
replaced
1028 *} |
1028 *} |
1029 |
1029 |
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) = |
|
1034 Type.raw_instance (ty1, Logic.varifyT ty2); |
|
1035 val qty_name = fst (dest_Type qty) |
1033 val qty_name = fst (dest_Type qty) |
1036 val SOME quotdata = quotdata_lookup lthy qty_name |
1034 val SOME quotdata = quotdata_lookup lthy qty_name |
1037 (* cu: Changed the lookup\<dots>not sure whether this works *) |
1035 (* cu: Changed the lookup\<dots>not sure whether this works *) |
1038 (* TODO: Should no longer be needed *) |
1036 (* TODO: Should no longer be needed *) |
1039 val rty = Logic.unvarifyT (#rtyp quotdata) |
1037 val rty = Logic.unvarifyT (#rtyp quotdata) |
1040 val rel = #rel quotdata |
1038 val rel = #rel quotdata |
1041 val rel_eqv = #equiv_thm quotdata |
1039 val rel_eqv = #equiv_thm quotdata |