--- a/Quot/QuotMain.thy Sat Dec 12 15:08:25 2009 +0100
+++ b/Quot/QuotMain.thy Sat Dec 12 15:23:58 2009 +0100
@@ -287,29 +287,30 @@
if rel' = rel then rtrm else raise exc
end
- | (_, Const (s, Type(st, _))) =>
+ | (_, Const _) =>
let
- fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
+ fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*)
| same_name _ _ = false
+ (* TODO/FIXME: This test is not enough. *)
+ (* Why? *)
+ (* Because constants can have the same name but not be the same
+ constant. All overloaded constants have the same name but because
+ of different types they do differ.
+
+ This code will let one write a theorem where plus on nat is
+ matched to plus on int, even if the latter is defined differently.
+
+ This would result in hard to understand failures in injection and
+ cleaning. *)
+ (* cu: if I also test the type, then something else breaks *)
in
- (* TODO/FIXME: This test is not enough. *)
- (* Why? *)
-(* Because constants can have the same name but not be the same
- constant. All overloaded constants have the same name but because
- of different types they do differ.
-
- This code will let one write a theorem where plus on nat is
- matched to plus on int, even if the latter is defined differently.
-
- This would result in hard to understand failures in injection and
- cleaning.
-*)
if same_name rtrm qtrm then rtrm
else
let
- val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)")
- val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)")
val thy = ProofContext.theory_of lthy
+ val qtrm_str = Syntax.string_of_term lthy qtrm
+ val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
+ val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
in
if Pattern.matches thy (rtrm', rtrm)