# HG changeset patch
# User wenzelm
# Date 1027971562 -7200
# Node ID ab814c7685a957363d87b2dd327ac8c3fbe133c4
# Parent  2232810416fcbc1cd60aa0b458e4a2f69dbdc646
tuned messages;

diff -r 2232810416fc -r ab814c7685a9 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jul 29 18:07:53 2002 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jul 29 21:39:22 2002 +0200
@@ -1033,14 +1033,14 @@
       handle TERM _ => err "Not a meta-equality (==)";
     val (f, xs) = Term.strip_comb lhs;
     val (c, _) = Term.dest_Free f handle TERM _ =>
-      err "Head of lhs must be free or fixed variable";
+      err "Head of lhs must be a free/fixed variable";
 
     fun is_free (Free (x, _)) = not (is_fixed ctxt x)
       | is_free _ = false;
     val extra_frees = filter is_free (term_frees rhs) \\ xs;
   in
     conditional (not (forall (is_Bound orf is_free) xs andalso null (duplicates xs))) (fn () =>
-      err "Arguments of lhs must be distinct free or fixed variables");
+      err "Arguments of lhs must be distinct free/bound variables");
     conditional (f mem Term.term_frees rhs) (fn () =>
       err "Element to be defined occurs on rhs");
     conditional (not (null extra_frees)) (fn () =>