src/Pure/drule.ML
changeset 655 9748dbcd4157
parent 641 49fc43cd6a35
child 668 0d0923eb0f0d
     1.1 --- a/src/Pure/drule.ML	Tue Oct 25 13:13:52 1994 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Oct 25 13:15:34 1994 +0100
     1.3 @@ -147,7 +147,7 @@
     1.4      val (c, ty) = dest_Const head
     1.5        handle TERM _ => err "Head of lhs not a constant";
     1.6  
     1.7 -    fun occs_const (Const (c', _)) = (c = c')
     1.8 +    fun occs_const (Const c_ty') = (c_ty' = (c, ty))
     1.9        | occs_const (Abs (_, _, t)) = occs_const t
    1.10        | occs_const (t $ u) = occs_const t orelse occs_const u
    1.11        | occs_const _ = false;
    1.12 @@ -168,7 +168,7 @@
    1.13      else if not (null rhs_extrasT) then
    1.14        err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
    1.15      else if occs_const rhs then
    1.16 -      err ("Constant " ^ quote c ^ " occurs on rhs")
    1.17 +      err ("Constant to be defined occurs on rhs")
    1.18      else (c, ty)
    1.19    end;
    1.20