equal
deleted
inserted
replaced
210 val thy = ProofContext.theory_of ctxt |
210 val thy = ProofContext.theory_of ctxt |
211 |
211 |
212 fun map_check_aux rty warns = |
212 fun map_check_aux rty warns = |
213 case rty of |
213 case rty of |
214 Type (_, []) => warns |
214 Type (_, []) => warns |
215 | Type (s, _) => if (maps_exists thy s) then warns else s::warns |
215 | Type (s, _) => if (maps_defined thy s) then warns else s::warns |
216 | _ => warns |
216 | _ => warns |
217 |
217 |
218 val warns = map_check_aux rty [] |
218 val warns = map_check_aux rty [] |
219 in |
219 in |
220 if null warns then () |
220 if null warns then () |