# HG changeset patch
# User wenzelm
# Date 1180905416 -7200
# Node ID 05fb9b2b16d73bf440c7e5bece7be8aabe4805be
# Parent  96f86d377dd99ef2d681bf82215bf7c7a0dc5d01
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);

diff -r 96f86d377dd9 -r 05fb9b2b16d7 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Jun 03 23:16:55 2007 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Jun 03 23:16:56 2007 +0200
@@ -124,6 +124,15 @@
 structure Locale: LOCALE =
 struct
 
+(* legacy operations *)
+
+fun gen_merge_lists _ xs [] = xs
+  | gen_merge_lists _ [] ys = ys
+  | gen_merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
+
+fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
+fun merge_alists xs = gen_merge_lists (eq_fst (op =)) xs;
+
 fun legacy_unvarifyT thm =
   let
     val cT = Thm.ctyp_of (Thm.theory_of_thm thm);