# HG changeset patch
# User wenzelm
# Date 1140282503 -3600
# Node ID 0eb600479944e3847ba608b57d04979395914c33
# Parent  db27ca6a6cd6912ad43d1d70f8c5956266fe8e54
dest_def: tuned error msg;

diff -r db27ca6a6cd6 -r 0eb600479944 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Feb 17 20:03:21 2006 +0100
+++ b/src/Pure/logic.ML	Sat Feb 18 18:08:23 2006 +0100
@@ -202,6 +202,11 @@
 
 (** definitions **)
 
+fun term_kind (Const _) = "existing constant "
+  | term_kind (Free _) = "free variable "
+  | term_kind (Bound _) = "bound variable "
+  | term_kind _ = "";
+
 (*c x == t[x] to !!x. c x == t[x]*)
 fun dest_def pp check_head is_fixed is_fixedT eq =
   let
@@ -234,7 +239,7 @@
       else insert (op =) v | _ => I)) rhs [];
   in
     if not (check_head head) then
-      err ("Bad head of lhs: " ^ display_terms [head])
+      err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
     else if not (null lhs_bads) then
       err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
     else if not (null lhs_dups) then