Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/logic.ML
changeset 4667 6328d427a339
parent 4631 c7fa4ae34495
child 4679 24917efb31b5 
--- a/src/Pure/logic.ML	Fri Feb 27 11:21:28 1998 +0100
+++ b/src/Pure/logic.ML	Sat Feb 28 15:40:03 1998 +0100
@@ -324,11 +324,11 @@
   orelse
    (null prems andalso
     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
-  orelse
+(*  orelse
    (case lhs of
       (f as Free _) $ (Var _) => exists (fn p => f occs p) prems orelse
                                  (null prems andalso f occs rhs)
-    | _ => false);
+    | _ => 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:
isabelle