--- 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:
--- 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