src/Pure/logic.ML
changeset 4631 c7fa4ae34495
parent 4443 d55e85d7f0c2
child 4667 6328d427a339
     1.1 --- a/src/Pure/logic.ML	Wed Feb 18 10:37:48 1998 +0100
     1.2 +++ b/src/Pure/logic.ML	Wed Feb 18 11:31:25 1998 +0100
     1.3 @@ -161,11 +161,7 @@
     1.4  
     1.5  (*Does t occur in u?  Or is alpha-convertible to u?
     1.6    The term t must contain no loose bound variables*)
     1.7 -fun t occs u = (t aconv u) orelse 
     1.8 -      (case u of
     1.9 -          Abs(_,_,body) => t occs body
    1.10 -	| f$t' => t occs f  orelse  t occs t'
    1.11 -	| _ => false);
    1.12 +fun t occs u = exists_subterm (fn s => t aconv s) u;
    1.13  
    1.14  (*Close up a formula over all free variables by quantification*)
    1.15  fun close_form A =
    1.16 @@ -327,11 +323,18 @@
    1.17     (exists (apl (lhs, op occs)) (rhs :: prems))
    1.18    orelse
    1.19     (null prems andalso
    1.20 -    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
    1.21 -(*the condition "null prems" in the last case is necessary because
    1.22 +    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
    1.23 +  orelse
    1.24 +   (case lhs of
    1.25 +      (f as Free _) $ (Var _) => exists (fn p => f occs p) prems orelse
    1.26 +                                 (null prems andalso f occs rhs)
    1.27 +    | _ => false);
    1.28 +(*the condition "null prems" in the last cases is necessary because
    1.29    conditional rewrites with extra variables in the conditions may terminate
    1.30    although the rhs is an instance of the lhs. Example:
    1.31    ?m < ?n ==> f(?n) == f(?m)*)
    1.32 +(*FIXME: proper test: lhs does not match a subterm of a premise
    1.33 +                      and does not match a subterm of the rhs if null prems *)
    1.34  
    1.35  fun rewrite_rule_extra_vars prems elhs erhs =
    1.36    if not ((term_vars erhs) subset