1.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Aug 13 14:45:07 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Aug 13 16:40:47 2010 +0200
     1.3 @@ -648,8 +648,9 @@
     1.4    from refs_def Node have refs_of'_ps: "refs_of' h ps refs"
     1.5      by (auto simp add: refs_of'_def'[symmetric])
     1.6    from validHeap refs_def have all_ref_present: "\<forall>r\<in>set refs. Ref.present h r" by simp
     1.7 -  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)"
     1.8 -    by (fastsimp elim!: crel_ref dest: refs_of'_is_fun)
     1.9 +  from init refs_of'_ps this
    1.10 +    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)"
    1.11 +    by (auto elim!: crel_ref [where ?'a="'a node", where ?'b="'a node", where ?'c="'a node"] dest: refs_of'_is_fun)
    1.12    from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" .
    1.13    with init have refs_of_p: "refs_of' h2 p (p#refs)"
    1.14      by (auto elim!: crel_refE simp add: refs_of'_def')