Added comment to function "loops".

--- a/src/Pure/thm.ML	Tue Apr 11 11:20:43 1995 +0200
+++ b/src/Pure/thm.ML	Tue Apr 11 12:01:11 1995 +0200
@@ -1072,6 +1072,11 @@
   orelse
    (null(prems) andalso
     Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs));
+(* the condition "null(prems)" in the last case is necessary because
+   conditional rewrites with extra variables in the conditions may terminate
+   although the rhs is an instance of the lhs. Example:
+   ?m < ?n ==> f(?n) == f(?m)
+*)
 
 fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) =
   let val prems = Logic.strip_imp_prems prop