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: