Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Library.is_equal;
authorwenzelm
Tue, 15 Apr 2008 16:12:15 +0200
changeset 26656 62fff5feb756
parent 26655 750bab48223d
child 26657 35249f5367b3
Library.is_equal;
src/Pure/General/file.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/rule_cases.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/General/file.ML	Tue Apr 15 16:12:13 2008 +0200
+++ b/src/Pure/General/file.ML	Tue Apr 15 16:12:15 2008 +0200
@@ -141,7 +141,7 @@
 
 fun eq paths =
   (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
-    SOME ids => OS.FileSys.compare ids = EQUAL
+    SOME ids => is_equal (OS.FileSys.compare ids)
   | NONE => false);
 
 fun copy src dst =
--- a/src/Pure/Isar/rule_cases.ML	Tue Apr 15 16:12:13 2008 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Tue Apr 15 16:12:15 2008 +0200
@@ -321,7 +321,7 @@
 local
 
 fun equal_cterms ts us =
-  list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us) = EQUAL;
+  is_equal (list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us));
 
 fun prep_rule n th =
   let
isabelle