285 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
285 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
286 in |
286 in |
287 if rel' = rel then rtrm else raise exc |
287 if rel' = rel then rtrm else raise exc |
288 end |
288 end |
289 |
289 |
290 | (_, Const (s, Type(st, _))) => |
290 | (_, Const _) => |
291 let |
291 let |
292 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
292 fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*) |
293 | same_name _ _ = false |
293 | same_name _ _ = false |
|
294 (* TODO/FIXME: This test is not enough. *) |
|
295 (* Why? *) |
|
296 (* Because constants can have the same name but not be the same |
|
297 constant. All overloaded constants have the same name but because |
|
298 of different types they do differ. |
|
299 |
|
300 This code will let one write a theorem where plus on nat is |
|
301 matched to plus on int, even if the latter is defined differently. |
|
302 |
|
303 This would result in hard to understand failures in injection and |
|
304 cleaning. *) |
|
305 (* cu: if I also test the type, then something else breaks *) |
294 in |
306 in |
295 (* TODO/FIXME: This test is not enough. *) |
|
296 (* Why? *) |
|
297 (* Because constants can have the same name but not be the same |
|
298 constant. All overloaded constants have the same name but because |
|
299 of different types they do differ. |
|
300 |
|
301 This code will let one write a theorem where plus on nat is |
|
302 matched to plus on int, even if the latter is defined differently. |
|
303 |
|
304 This would result in hard to understand failures in injection and |
|
305 cleaning. |
|
306 *) |
|
307 if same_name rtrm qtrm then rtrm |
307 if same_name rtrm qtrm then rtrm |
308 else |
308 else |
309 let |
309 let |
310 val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)") |
|
311 val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)") |
|
312 val thy = ProofContext.theory_of lthy |
310 val thy = ProofContext.theory_of lthy |
|
311 val qtrm_str = Syntax.string_of_term lthy qtrm |
|
312 val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") |
|
313 val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") |
313 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
314 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
314 in |
315 in |
315 if Pattern.matches thy (rtrm', rtrm) |
316 if Pattern.matches thy (rtrm', rtrm) |
316 then rtrm else raise exc2 |
317 then rtrm else raise exc2 |
317 end |
318 end |