# HG changeset patch
# User wenzelm
# Date 783087334 -3600
# Node ID 9748dbcd4157692ab50f6622412fdd9c4ba5fd36
# Parent  65435e2c6512676363824e16934d49f007fe26e8
minor change of occs_const in dest_defn;

diff -r 65435e2c6512 -r 9748dbcd4157 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Oct 25 13:13:52 1994 +0100
+++ b/src/Pure/drule.ML	Tue Oct 25 13:15:34 1994 +0100
@@ -147,7 +147,7 @@
     val (c, ty) = dest_Const head
       handle TERM _ => err "Head of lhs not a constant";
 
-    fun occs_const (Const (c', _)) = (c = c')
+    fun occs_const (Const c_ty') = (c_ty' = (c, ty))
       | occs_const (Abs (_, _, t)) = occs_const t
       | occs_const (t $ u) = occs_const t orelse occs_const u
       | occs_const _ = false;
@@ -168,7 +168,7 @@
     else if not (null rhs_extrasT) then
       err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
     else if occs_const rhs then
-      err ("Constant " ^ quote c ^ " occurs on rhs")
+      err ("Constant to be defined occurs on rhs")
     else (c, ty)
   end;