--- a/src/Pure/thm.ML Thu Sep 29 00:59:00 2005 +0200
+++ b/src/Pure/thm.ML Thu Sep 29 00:59:01 2005 +0200
@@ -396,7 +396,7 @@
(*attributes subsume any kind of rules or context modifiers*)
type 'a attribute = 'a * thm -> 'a * thm;
-
+
fun no_attributes x = (x, []);
fun simple_fact x = [(x, [])];
fun apply_attributes (x_th, atts) = Library.apply atts x_th;
@@ -814,6 +814,7 @@
(Cterm {t = x, T, sorts, ...})
(th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) =
let
+ val string_of = Sign.string_of_term (Theory.deref thy_ref);
val (t, u) = Logic.dest_equals prop
handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
val result =
@@ -827,13 +828,13 @@
(Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))};
fun check_occs x ts =
if exists (fn t => Logic.occs (x, t)) ts then
- raise THM ("abstract_rule: variable free in assumptions", 0, [th])
+ raise THM ("abstract_rule: variable free in assumptions " ^ string_of x, 0, [th])
else ();
in
case x of
Free _ => (check_occs x hyps; check_occs x (terms_of_tpairs tpairs); result)
| Var _ => (check_occs x (terms_of_tpairs tpairs); result)
- | _ => raise THM ("abstract_rule: not a variable", 0, [th])
+ | _ => raise THM ("abstract_rule: not a variable " ^ string_of x, 0, [th])
end;
(*The combination rule