1.1 --- a/src/Pure/logic.ML	Thu Jun 27 15:24:17 1996 +0200
     1.2 +++ b/src/Pure/logic.ML	Fri Jun 28 11:10:32 1996 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  
     1.5  (** equality **)
     1.6  
     1.7 -(*Make an equality.*)
     1.8 +(*Make an equality.  DOES NOT CHECK TYPE OF u*)
     1.9  fun mk_equals(t,u) = equals(fastype_of t) $ t $ u;
    1.10  
    1.11  fun dest_equals (Const("==",_) $ t $ u)  =  (t,u)