equal
deleted
inserted
replaced
152 list_comb (Const (relmap, dummyT), args) |
152 list_comb (Const (relmap, dummyT), args) |
153 end |
153 end |
154 else |
154 else |
155 let |
155 let |
156 val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")") |
156 val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")") |
157 val equiv_rel = #equiv_rel (quotdata_lookup_thy thy s') handle NotFound => raise exc |
157 val equiv_rel = #equiv_rel (quotdata_lookup thy s') handle NotFound => raise exc |
158 (* FIXME: check in this case that the rty and qty *) |
158 (* FIXME: check in this case that the rty and qty *) |
159 (* FIXME: correspond to each other *) |
159 (* FIXME: correspond to each other *) |
160 |
160 |
161 (* we need to instantiate the TVars in the relation *) |
161 (* we need to instantiate the TVars in the relation *) |
162 val thy = ProofContext.theory_of ctxt |
162 val thy = ProofContext.theory_of ctxt |