src/Pure/thm.ML

         maxidx = maxidx,
         shyps = Sorts.union sorts shyps,
         hyps = hyps,
         tpairs = tpairs,
         prop = all T $ Abs (a, T, abstract_over (x, prop))};
-    fun check_occs x ts =
+    fun check_occs a x ts =
       if exists (fn t => Logic.occs (x, t)) ts then
-        raise THM("forall_intr: variable free in assumptions", 0, [th])
+        raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
       else ();
   in
     case x of
-      Free (a, _) => (check_occs x hyps; check_occs x (terms_of_tpairs tpairs); result a)
-    | Var ((a, _), _) => (check_occs x (terms_of_tpairs tpairs); result a)
+      Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a)
+    | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a)
     | _ => raise THM ("forall_intr: not a variable", 0, [th])
   end;
 
 (*Forall elimination
   !!x. A

 *)
 fun abstract_rule a
     (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 =
       Thm {thy_ref = thy_ref,
         der = Pt.infer_derivs' (Pt.abstract_rule x a) der,

         shyps = Sorts.union sorts shyps,
         hyps = hyps,
         tpairs = tpairs,
         prop = Logic.mk_equals
           (Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))};
-    fun check_occs x ts =
+    fun check_occs a x ts =
       if exists (fn t => Logic.occs (x, t)) ts then
-        raise THM ("abstract_rule: variable free in assumptions " ^ string_of x, 0, [th])
+        raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 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 " ^ string_of x, 0, [th])
+      Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result)
+    | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result)
+    | _ => raise THM ("abstract_rule: not a variable", 0, [th])
   end;
 
 (*The combination rule
   f == g  t == u
   --------------