# HG changeset patch
# User haftmann
# Date 1281710447 -7200
# Node ID 8e4058f4848c309bbae2cb08d6b05c27704154cf
# Parent  9ee71ec7db4e01d3520ae0eef033745902848c97
robustified proof

diff -r 9ee71ec7db4e -r 8e4058f4848c src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Aug 13 14:45:07 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Aug 13 16:40:47 2010 +0200
@@ -648,8 +648,9 @@
   from refs_def Node have refs_of'_ps: "refs_of' h ps refs"
     by (auto simp add: refs_of'_def'[symmetric])
   from validHeap refs_def have all_ref_present: "\<forall>r\<in>set refs. Ref.present h r" by simp
-  from init refs_of'_ps Node this have heap_eq: "\<forall>refs. refs_of' h ps refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)"
-    by (fastsimp elim!: crel_ref dest: refs_of'_is_fun)
+  from init refs_of'_ps this
+    have heap_eq: "\<forall>refs. refs_of' h ps refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)"
+    by (auto elim!: crel_ref [where ?'a="'a node", where ?'b="'a node", where ?'c="'a node"] dest: refs_of'_is_fun)
   from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" .
   with init have refs_of_p: "refs_of' h2 p (p#refs)"
     by (auto elim!: crel_refE simp add: refs_of'_def')