# HG changeset patch
# User haftmann
# Date 1161614961 -7200
# Node ID d0d8a48ae4e68dfcd4df94483e1ea1f5a39dd6e9
# Parent  5a59f8ff96cc854006af52e7e948075b13a53544
switched merge_alists'' to AList.merge'' whenever appropriate

diff -r 5a59f8ff96cc -r d0d8a48ae4e6 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Mon Oct 23 11:18:50 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Mon Oct 23 16:49:21 2006 +0200
@@ -54,7 +54,7 @@
 
 fun pretty_hints ({simps, congs, wfs}: hints) =
  [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm simps),
-  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm (map #2 congs)),
+  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm (map snd congs)),
   Pretty.big_list "recdef wf hints:" (map Display.pretty_thm wfs)];
 
 
@@ -71,14 +71,20 @@
 in
 
 fun add_cong raw_thm congs =
-  let val (c, thm) = prep_cong raw_thm
-  in overwrite_warn (congs, (c, thm)) ("Overwriting recdef congruence rule for " ^ quote c) end;
+  let
+    val (c, thm) = prep_cong raw_thm;
+    val _ = if AList.defined (op =) congs c
+      then warning ("Overwriting recdef congruence rule for " ^ quote c)
+      else ();
+  in AList.update (op =) (c, thm) congs end;
 
 fun del_cong raw_thm congs =
   let
     val (c, thm) = prep_cong raw_thm;
-    val (del, rest) = List.partition (Library.equal c o fst) congs;
-  in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
+    val _ = if AList.defined (op =) congs c
+      then ()
+      else warning ("No recdef congruence rule for " ^ quote c);
+  in AList.delete (op =) c congs end;
 
 end;
 
@@ -103,7 +109,7 @@
     (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
       (Symtab.merge (K true) (tab1, tab2),
         mk_hints (Drule.merge_rules (simps1, simps2),
-          Library.merge_alists congs1 congs2,
+          AList.merge (op =) eq_thm (congs1, congs2),
           Drule.merge_rules (wfs1, wfs2)));
 
   fun print thy (tab, hints) =
@@ -194,13 +200,13 @@
     val {simps, congs, wfs} = get_local_hints ctxt;
     val cs = local_claset_of ctxt;
     val ss = local_simpset_of ctxt addsimps simps;
-  in (cs, ss, map #2 congs, wfs) end;
+  in (cs, ss, rev (map snd congs), wfs) end;
 
 fun prepare_hints_i thy () =
   let
     val ctxt0 = ProofContext.init thy;
     val {simps, congs, wfs} = get_global_hints thy;
-  in (local_claset_of ctxt0, local_simpset_of ctxt0 addsimps simps, map #2 congs, wfs) end;
+  in (local_claset_of ctxt0, local_simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
 
 
 
@@ -226,7 +232,7 @@
     val (thy, {rules = rules_idx, induct, tcs}) =
         tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
-    val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
+    val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     val simp_att = if null tcs then [Simplifier.simp_add, RecfunCodegen.add NONE] else [];
 
     val ((simps' :: rules', [induct']), thy) =
diff -r 5a59f8ff96cc -r d0d8a48ae4e6 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Mon Oct 23 11:18:50 2006 +0200
+++ b/src/HOL/Tools/refute.ML	Mon Oct 23 16:49:21 2006 +0200
@@ -187,8 +187,8 @@
 		fun merge _
 			({interpreters = in1, printers = pr1, parameters = pa1},
 			 {interpreters = in2, printers = pr2, parameters = pa2}) =
-			{interpreters = rev (merge_alists (rev in1) (rev in2)),
-			 printers = rev (merge_alists (rev pr1) (rev pr2)),
+			{interpreters = AList.merge (op =) (K true) (in1, in2),
+			 printers = AList.merge (op =) (K true) (pr1, pr2),
 			 parameters = Symtab.merge (op=) (pa1, pa2)};
 		fun print sg {interpreters, printers, parameters} =
 			Pretty.writeln (Pretty.chunks
diff -r 5a59f8ff96cc -r d0d8a48ae4e6 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Oct 23 11:18:50 2006 +0200
+++ b/src/Pure/codegen.ML	Mon Oct 23 16:49:21 2006 +0200
@@ -229,9 +229,9 @@
       preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
     {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
      tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
-     consts = merge_alists consts1 consts2,
-     types = merge_alists types1 types2,
-     attrs = merge_alists attrs1 attrs2,
+     consts = AList.merge (op =) (K true) (consts1, consts2),
+     types = AList.merge (op =) (K true) (types1, types2),
+     attrs = AList.merge (op =) (K true) (attrs1, attrs2),
      preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
      modules = Symtab.merge (K true) (modules1, modules2),
      test_params = merge_test_params test_params1 test_params2};
@@ -418,7 +418,7 @@
     | _ => error ("Not a type constructor: " ^ s)
   end) (thy, xs);
 
-fun get_assoc_type thy s = AList.lookup (op =) ((#types o CodegenData.get) thy) s;
+fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy);
 
 
 (**** make valid ML identifiers ****)