no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property

--- a/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -2052,7 +2052,7 @@
     let ?v = "Neg e"
     have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))"
       by simp
-    from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
+    from 7(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
     have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)"
       by auto
     from H p have "x + ?e > 0 \<and> x + ?e \<le> d"
@@ -2085,7 +2085,7 @@
     let ?v = "Sub (C -1) e"
     have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))"
       by simp
-    from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
+    from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
     have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e - 1 + j)"
       by auto
     from H p have "x + ?e \<ge> 0 \<and> x + ?e < d"

--- a/src/HOL/Decision_Procs/MIR.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -2612,7 +2612,7 @@
     {assume H: "\<not> real (x-d) + ?e > 0" 
       let ?v="Neg e"
       have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
-      from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 
+      from 7(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 
       have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x =  - ?e + real j)" by auto 
       from H p have "real x + ?e > 0 \<and> real x + ?e \<le> real d" by (simp add: c1)
       hence "real (x + floor ?e) > real (0::int) \<and> real (x + floor ?e) \<le> real d"
@@ -2638,7 +2638,7 @@
     {assume H: "\<not> real (x-d) + ?e \<ge> 0" 
       let ?v="Sub (C -1) e"
       have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
-      from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 
+      from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 
       have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x =  - ?e - 1 + real j)" by auto 
       from H p have "real x + ?e \<ge> 0 \<and> real x + ?e < real d" by (simp add: c1)
       hence "real (x + floor ?e) \<ge> real (0::int) \<and> real (x + floor ?e) < real d"
@@ -3394,7 +3394,7 @@
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un 
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {n .. 0})))"
-    by (simp only: set_map set_upto set_simps)
+    by (simp only: set_map set_upto list.set)
   also have "\<dots> =   
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un 
@@ -3548,7 +3548,7 @@
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un 
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {n .. 0})))"
-    by (simp only: set_map set_upto set_simps)
+    by (simp only: set_map set_upto list.set)
   also have "\<dots> =   
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un 

--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -642,7 +642,7 @@
   with init all_ref_present have q_is_new: "q \<notin> set (p#refs)"
     by (auto elim!: effect_refE intro!: Ref.noteq_I)
   from refs_of_p refs_of_q q_is_new have a3: "\<forall>qrs prs. refs_of' h2 q qrs \<and> refs_of' h2 p prs \<longrightarrow> set prs \<inter> set qrs = {}"
-    by (fastforce simp only: set_simps dest: refs_of'_is_fun)
+    by (fastforce simp only: list.set dest: refs_of'_is_fun)
   from rev'_invariant [OF effect_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" 
     unfolding list_of'_def by auto
   with lookup show ?thesis

--- a/src/HOL/Library/Permutation.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Library/Permutation.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -162,7 +162,7 @@
   apply (case_tac "remdups xs")
    apply simp_all
   apply (subgoal_tac "a \<in> set (remdups ys)")
-   prefer 2 apply (metis set_simps(2) insert_iff set_remdups)
+   prefer 2 apply (metis list.set(2) insert_iff set_remdups)
   apply (drule split_list) apply (elim exE conjE)
   apply (drule_tac x = list in spec) apply (erule impE) prefer 2
    apply (drule_tac x = "ysa @ zs" in spec) apply (erule impE) prefer 2

--- a/src/HOL/Library/RBT_Set.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -522,7 +522,7 @@
 
 code_datatype Set Coset
 
-declare set_simps[code]
+declare list.set[code] (* needed? *)
 
 lemma empty_Set [code]:
   "Set.empty = Set RBT.empty"

--- a/src/HOL/List.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/List.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -39,6 +39,8 @@
 
 setup {* Sign.parent_path *}
 
+lemmas set_simps = list.set (* legacy *)
+
 syntax
   -- {* list Enumeration *}
   "_list" :: "args => 'a list"    ("[(_)]")
@@ -54,16 +56,9 @@
 "last (x # xs) = (if xs = [] then x else last xs)"
 
 primrec butlast :: "'a list \<Rightarrow> 'a list" where
-"butlast []= []" |
+"butlast [] = []" |
 "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
 
-declare list.set[simp del, code del]
-
-lemma set_simps[simp, code, code_post]:
-  "set [] = {}"
-  "set (x # xs) = insert x (set xs)"
-by (simp_all add: list.set)
-
 lemma set_rec: "set xs = rec_list {} (\<lambda>x _. insert x) xs"
   by (induct xs) auto
 
@@ -575,7 +570,7 @@
 
 fun simproc ctxt redex =
   let
-    val set_Nil_I = @{thm trans} OF [@{thm set_simps(1)}, @{thm empty_def}]
+    val set_Nil_I = @{thm trans} OF [@{thm list.set(1)}, @{thm empty_def}]
     val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
     val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
     val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
@@ -1255,6 +1250,8 @@
 
 subsubsection {* @{const set} *}
 
+declare list.set[code_post]  --"pretty output"
+
 lemma finite_set [iff]: "finite (set xs)"
 by (induct xs) auto
 
@@ -1404,7 +1401,7 @@
 
 
 lemma finite_list: "finite A ==> EX xs. set xs = A"
-  by (erule finite_induct) (auto simp add: set_simps(2) [symmetric] simp del: set_simps(2))
+  by (erule finite_induct) (auto simp add: list.set(2)[symmetric] simp del: list.set(2))
 
 lemma card_length: "card (set xs) \<le> length xs"
 by (induct xs) (auto simp add: card_insert_if)

--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -1392,7 +1392,7 @@
 
   apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
     apply (rule max_of_list_sublist)
-    apply (simp (no_asm_simp) only: set_append set_simps list.map) apply blast
+    apply (simp (no_asm_simp) only: set_append list.set list.map) apply blast
   apply (simp (no_asm_simp))
   apply simp                    (* subgoal bc3 = [] *)
   apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
@@ -1419,7 +1419,7 @@
      (* (some) preconditions of  wt_instr_offset *)
   apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
   apply (rule max_of_list_sublist)
-    apply (simp (no_asm_simp) only: set_append set_simps list.map) apply blast
+    apply (simp (no_asm_simp) only: set_append list.set list.map) apply blast
   apply (simp (no_asm_simp))
 
 apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)

--- a/src/HOL/Quotient_Examples/FSet.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -985,7 +985,7 @@
   have b: "\<And>x' ys'. \<lbrakk>\<not> List.member ys' x'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
   have c: "xs = [] \<Longrightarrow> thesis" using b 
     apply(simp)
-    by (metis List.set_simps(1) emptyE empty_subsetI)
+    by (metis list.set(1) emptyE empty_subsetI)
   have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
   proof -
     fix x :: 'a

--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -151,7 +151,7 @@
   using filter_filter [Transfer.transferred] .
 
 lemma "fset (fcons x xs) = insert x (fset xs)"
-  using set_simps(2) [Transfer.transferred] .
+  using list.set(2) [Transfer.transferred] .
 
 lemma "fset (fappend xs ys) = fset xs \<union> fset ys"
   using set_append [Transfer.transferred] .