equal
deleted
inserted
replaced
292 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
292 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
293 | same_name _ _ = false |
293 | same_name _ _ = false |
294 in |
294 in |
295 (* TODO/FIXME: This test is not enough. *) |
295 (* TODO/FIXME: This test is not enough. *) |
296 (* Why? *) |
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 *) |
297 if same_name rtrm qtrm then rtrm |
307 if same_name rtrm qtrm then rtrm |
298 else |
308 else |
299 let |
309 let |
300 val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)") |
310 val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)") |
301 val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)") |
311 val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)") |