--- a/src/HOL/More_Set.thy Fri Jan 06 11:15:02 2012 +0100
+++ b/src/HOL/More_Set.thy Fri Jan 06 20:39:50 2012 +0100
@@ -4,7 +4,7 @@
header {* Relating (finite) sets and lists *}
theory More_Set
-imports More_List
+imports List
begin
lemma comp_fun_idem_remove: