equal
deleted
inserted
replaced
126 error (implode ["Quotient type ", qtystr, " does not match with ", rtystr]) |
126 error (implode ["Quotient type ", qtystr, " does not match with ", rtystr]) |
127 end |
127 end |
128 |
128 |
129 fun sanity_chk lthy qenv = |
129 fun sanity_chk lthy qenv = |
130 let |
130 let |
131 val qenv' = Quotient_Info.mk_qenv lthy |
131 val global_qenv = Quotient_Info.mk_qenv lthy |
132 val thy = ProofContext.theory_of lthy |
132 val thy = ProofContext.theory_of lthy |
133 |
133 |
134 fun is_inst thy (qty, rty) (qty', rty') = |
134 fun is_inst thy (qty, rty) (qty', rty') = |
135 if Sign.typ_instance thy (qty, qty') |
135 if Sign.typ_instance thy (qty, qty') |
136 then let |
136 then let |
139 rty = Envir.subst_type inst rty' |
139 rty = Envir.subst_type inst rty' |
140 end |
140 end |
141 else false |
141 else false |
142 |
142 |
143 fun chk_inst (qty, rty) = |
143 fun chk_inst (qty, rty) = |
144 if exists (is_inst thy (qty, rty)) qenv' then true |
144 if exists (is_inst thy (qty, rty)) global_qenv |
|
145 then true |
145 else error_msg lthy (qty, rty) |
146 else error_msg lthy (qty, rty) |
146 in |
147 in |
147 forall chk_inst qenv |
148 forall chk_inst qenv |
148 end |
149 end |
149 |
150 |