diff -r e81d0f04ffdf -r c04f8c51d0ab src/HOL/Library/List_Set.thy --- a/src/HOL/Library/List_Set.thy Mon Jun 29 12:18:56 2009 +0200 +++ b/src/HOL/Library/List_Set.thy Mon Jun 29 12:18:57 2009 +0200 @@ -160,4 +160,7 @@ "A \ B = project (\x. x \ A) B" by (auto simp add: project_def) + +hide (open) const insert + end \ No newline at end of file