# HG changeset patch
# User bulwahn
# Date 1323876632 -3600
# Node ID 37ffb8797a6398b608f457b0caf70de50e665146
# Parent  3759fb8a02b81cd530c67b4186a1c4b55a2b71d5
correcting dependencies after renaming

diff -r 3759fb8a02b8 -r 37ffb8797a63 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Dec 14 16:30:30 2011 +0100
+++ b/src/HOL/IsaMakefile	Wed Dec 14 16:30:32 2011 +0100
@@ -435,7 +435,7 @@
 $(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML				\
   $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
   Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
-  Library/AList.thy Library/AList_Mapping.thy 				\
+  Library/AList_Impl.thy Library/AList_Mapping.thy 			\
   Library/BigO.thy Library/Binomial.thy 				\
   Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
   Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
diff -r 3759fb8a02b8 -r 37ffb8797a63 src/HOL/Library/AList_Mapping.thy
--- a/src/HOL/Library/AList_Mapping.thy	Wed Dec 14 16:30:30 2011 +0100
+++ b/src/HOL/Library/AList_Mapping.thy	Wed Dec 14 16:30:32 2011 +0100
@@ -5,7 +5,7 @@
 header {* Implementation of mappings with Association Lists *}
 
 theory AList_Mapping
-imports AList Mapping
+imports AList_Impl Mapping
 begin
 
 definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where