Improved loop-test for rewrite rules a little.
Should be done properly!

--- a/src/Pure/logic.ML	Wed Feb 18 10:37:48 1998 +0100
+++ b/src/Pure/logic.ML	Wed Feb 18 11:31:25 1998 +0100
@@ -161,11 +161,7 @@
 
 (*Does t occur in u?  Or is alpha-convertible to u?
   The term t must contain no loose bound variables*)
-fun t occs u = (t aconv u) orelse 
-      (case u of
-          Abs(_,_,body) => t occs body
-	| f$t' => t occs f  orelse  t occs t'
-	| _ => false);
+fun t occs u = exists_subterm (fn s => t aconv s) u;
 
 (*Close up a formula over all free variables by quantification*)
 fun close_form A =
@@ -327,11 +323,18 @@
    (exists (apl (lhs, op occs)) (rhs :: prems))
   orelse
    (null prems andalso
-    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
-(*the condition "null prems" in the last case is necessary because
+    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
+  orelse
+   (case lhs of
+      (f as Free _) $ (Var _) => exists (fn p => f occs p) prems orelse
+                                 (null prems andalso f occs rhs)
+    | _ => false);
+(*the condition "null prems" in the last cases 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)*)
+(*FIXME: proper test: lhs does not match a subterm of a premise
+                      and does not match a subterm of the rhs if null prems *)
 
 fun rewrite_rule_extra_vars prems elhs erhs =
   if not ((term_vars erhs) subset

--- a/src/Pure/term.ML	Wed Feb 18 10:37:48 1998 +0100
+++ b/src/Pure/term.ML	Wed Feb 18 11:31:25 1998 +0100
@@ -154,6 +154,7 @@
   val add_term_vars: term * term list -> term list
   val term_vars: term -> term list
   val exists_Const: (string * typ -> bool) -> term -> bool
+  val exists_subterm: (term -> bool) -> term -> bool
   val compress_type: typ -> typ
   val compress_term: term -> term
 end;
@@ -729,6 +730,14 @@
 	|   ex _               = false
     in ex t end;
 
+fun exists_subterm P =
+  let fun ex t = P t orelse
+                 (case t of
+                    u $ v        => ex u orelse ex v
+                  | Abs(_, _, u) => ex u
+                  | _            => false)
+  in ex end;
+
 (*map classes, tycons*)
 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
   | map_typ f _ (TFree (x, S)) = TFree (x, map f S)