abstract_rule: tuned exception msgs;

--- 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