# HG changeset patch
# User wenzelm
# Date 1295016184 -3600
# Node ID 2c65ad10bec88898cbc9be73f1feb78d883ae3d6
# Parent  bd0bebf93fa62fcceefe29d42b9672a10c520c3f
more precise import;
eliminated global prems;

diff -r bd0bebf93fa6 -r 2c65ad10bec8 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Jan 14 13:58:07 2011 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Jan 14 15:43:04 2011 +0100
@@ -5,7 +5,7 @@
 header {* Linked Lists by ML references *}
 
 theory Linked_Lists
-imports Imperative_HOL Code_Integer
+imports "../Imperative_HOL" Code_Integer
 begin
 
 section {* Definition of Linked Lists *}
@@ -371,13 +371,12 @@
 assumes "Ref.get h1 p = Node x pn"
 assumes "refs_of' (Ref.set p (Node x r1) h1) p rs"
 obtains r1s where "rs = (p#r1s)" and "refs_of' h1 r1 r1s"
-using assms
 proof -
   from assms refs_of'_distinct[OF assms(2)] have "\<exists> r1s. rs = (p # r1s) \<and> refs_of' h1 r1 r1s"
     apply -
     unfolding refs_of'_def'[of _ p]
     apply (auto, frule refs_of_set_ref2) by (auto dest: Ref.noteq_sym)
-  with prems show thesis by auto
+  with assms that show thesis by auto
 qed
 
 section {* Proving make_llist and traverse correct *}