diff -r 81061bd61ad3 -r 4699a9058a4f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Aug 12 16:26:02 1996 +0200
+++ b/src/Pure/drule.ML	Mon Aug 12 16:28:15 1996 +0200
@@ -137,7 +137,7 @@
     val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
   in
     if not (forall is_Free args) then
-      err "Arguments of lhs have to be variables"
+      err "Arguments (on lhs) must be variables"
     else if not (null lhs_dups) then
       err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
     else if not (null rhs_extras) then