diff -r 896f01fe825b -r db4045d1406e src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Mar 06 09:58:30 2010 +0100
+++ b/src/HOL/List.thy	Sat Mar 06 09:58:33 2010 +0100
@@ -290,6 +290,9 @@
 abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
 abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
 
+definition insort_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "insort_insert x xs = (if x \<in> set xs then xs else insort x xs)"
+
 end
 
 
@@ -3703,6 +3706,20 @@
   finally show "\<not> t < f x" by simp
 qed
 
+lemma set_insort_insert:
+  "set (insort_insert x xs) = insert x (set xs)"
+  by (auto simp add: insort_insert_def set_insort)
+
+lemma distinct_insort_insert:
+  assumes "distinct xs"
+  shows "distinct (insort_insert x xs)"
+  using assms by (induct xs) (auto simp add: insort_insert_def set_insort)
+
+lemma sorted_insort_insert:
+  assumes "sorted xs"
+  shows "sorted (insort_insert x xs)"
+  using assms by (simp add: insort_insert_def sorted_insort)
+
 end
 
 lemma sorted_upt[simp]: "sorted[i..<j]"