# HG changeset patch
# User wenzelm
# Date 1326543759 -3600
# Node ID d3d62b528487293d6ff230911f21b60b5e35f430
# Parent  07e334ad2e2a1aa79300f99f8893902dc815a583
tuned proofs;

diff -r 07e334ad2e2a -r d3d62b528487 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Sat Jan 14 13:11:32 2012 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Sat Jan 14 13:22:39 2012 +0100
@@ -328,9 +328,7 @@
 apply  auto
 apply(rule hconfI)
 apply(drule conforms_heapD)
-apply(tactic {*
-  auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}]
-    |> map_simpset (fn ss => ss delsimps [@{thm split_paired_All}])) *})
+apply(auto elim: oconf_hext dest: hconfD)
 done
 
 lemma conforms_upd_local: 
diff -r 07e334ad2e2a -r d3d62b528487 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Sat Jan 14 13:11:32 2012 +0100
+++ b/src/HOL/Unix/Unix.thy	Sat Jan 14 13:22:39 2012 +0100
@@ -1034,7 +1034,7 @@
                   lookup root ((path @ [y]) @ us) \<noteq> None"
                 by cases (auto dest: access_some_lookup)
               then show ?thesis 
-                by (simp, blast dest!: lookup_some_append)
+                by (fastforce dest!: lookup_some_append)
             qed
             finally show ?thesis .
           qed