--- 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 \
--- 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