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.
Merged.
authorballarin
Wed, 18 Mar 2009 22:17:23 +0100
changeset 30581 ac50e7dedf6d
parent 30580 cc5a55d7a5be (current diff)
parent 30572 8fbc355100f2 (diff)
child 30582 638b088bb840
child 30749 44a16c6956f9
Merged.
--- a/src/Pure/General/ord_list.ML	Wed Mar 18 22:14:58 2009 +0100
+++ b/src/Pure/General/ord_list.ML	Wed Mar 18 22:17:23 2009 +0100
@@ -85,7 +85,7 @@
             LESS => x :: handle_same (unio xs) lst2
           | EQUAL => y :: unio xs ys
           | GREATER => y :: unio lst1 ys);
-  in handle_same (unio list1) list2 end;
+  in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
 
 (*intersection: filter second list for elements present in first list*)
 nonfix inter;
--- a/src/Pure/library.ML	Wed Mar 18 22:14:58 2009 +0100
+++ b/src/Pure/library.ML	Wed Mar 18 22:17:23 2009 +0100
@@ -817,8 +817,10 @@
 
 fun subtract eq = fold (remove eq);
 
-fun merge _ ([], ys) = ys
-  | merge eq (xs, ys) = fold_rev (insert eq) ys xs;
+fun merge eq (xs, ys) =
+  if pointer_eq (xs, ys) then xs
+  else if null xs then ys
+  else fold_rev (insert eq) ys xs;
 
 
 (* old-style infixes *)
isabelle