# HG changeset patch
# User paulson
# Date 835953032 -7200
# Node ID 07eee14f5bd4bcf5a8f1b49f411d337d1f3601ae
# Parent  c780a4f39454bd3da4c658697ff1b56b9090998e
Restored warning comment

diff -r c780a4f39454 -r 07eee14f5bd4 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Jun 27 15:24:17 1996 +0200
+++ b/src/Pure/logic.ML	Fri Jun 28 11:10:32 1996 +0200
@@ -56,7 +56,7 @@
 
 (** equality **)
 
-(*Make an equality.*)
+(*Make an equality.  DOES NOT CHECK TYPE OF u*)
 fun mk_equals(t,u) = equals(fastype_of t) $ t $ u;
 
 fun dest_equals (Const("==",_) $ t $ u)  =  (t,u)