src/Pure/logic.ML
changeset 4667 6328d427a339
parent 4631 c7fa4ae34495
child 4679 24917efb31b5
     1.1 --- a/src/Pure/logic.ML	Fri Feb 27 11:21:28 1998 +0100
     1.2 +++ b/src/Pure/logic.ML	Sat Feb 28 15:40:03 1998 +0100
     1.3 @@ -324,11 +324,11 @@
     1.4    orelse
     1.5     (null prems andalso
     1.6      Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
     1.7 -  orelse
     1.8 +(*  orelse
     1.9     (case lhs of
    1.10        (f as Free _) $ (Var _) => exists (fn p => f occs p) prems orelse
    1.11                                   (null prems andalso f occs rhs)
    1.12 -    | _ => false);
    1.13 +    | _ => false)*);
    1.14  (*the condition "null prems" in the last cases is necessary because
    1.15    conditional rewrites with extra variables in the conditions may terminate
    1.16    although the rhs is an instance of the lhs. Example: