src/Pure/meta_simplifier.ML
changeset 16305 5e7b6731b004
parent 16042 8e15ff79851a
child 16378 8af448f67cef
     1.1 --- a/src/Pure/meta_simplifier.ML	Mon Jun 06 18:58:34 2005 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Jun 06 19:09:49 2005 +0200
     1.3 @@ -412,6 +412,12 @@
     1.4      orelse
     1.5    is_Var (head_of lhs)
     1.6      orelse
     1.7 +(* turns t = x around, which causes a headache if x is a local variable -
     1.8 +   usually it is very useful :-(
     1.9 +  is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
    1.10 +  andalso not(exists_subterm is_Var lhs)
    1.11 +    orelse
    1.12 +*)
    1.13    exists (apl (lhs, Logic.occs)) (rhs :: prems)
    1.14      orelse
    1.15    null prems andalso Pattern.matches (Sign.tsig_of sign) (lhs, rhs)