diff -r 5e845b75f94f -r 5e7b6731b004 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Jun 06 18:58:34 2005 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Jun 06 19:09:49 2005 +0200
@@ -412,6 +412,12 @@
     orelse
   is_Var (head_of lhs)
     orelse
+(* turns t = x around, which causes a headache if x is a local variable -
+   usually it is very useful :-(
+  is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
+  andalso not(exists_subterm is_Var lhs)
+    orelse
+*)
   exists (apl (lhs, Logic.occs)) (rhs :: prems)
     orelse
   null prems andalso Pattern.matches (Sign.tsig_of sign) (lhs, rhs)