--- a/src/HOL/Library/AList_Mapping.thy Tue Sep 13 09:25:19 2011 +0200
+++ b/src/HOL/Library/AList_Mapping.thy Tue Sep 13 09:28:03 2011 +0200
@@ -5,7 +5,7 @@
header {* Implementation of mappings with Association Lists *}
theory AList_Mapping
-imports AList_Impl Mapping
+imports AList Mapping
begin
definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
@@ -69,4 +69,4 @@
"HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
by (fact equal_refl)
-end
\ No newline at end of file
+end