diff -r a0134252ac29 -r a879f14b6f95 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Feb 19 22:02:23 2014 +1100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Feb 19 16:32:37 2014 +0100
@@ -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: set_simps 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