diff -r 85fb70b0c5e8 -r 88bee9f6eec7 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Fri May 13 22:55:00 2011 +0200
@@ -328,8 +328,9 @@
 apply  auto
 apply(rule hconfI)
 apply(drule conforms_heapD)
-apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}] 
-                addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *})
+apply(tactic {*
+  auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}]
+  |> map_simpset_local (fn ss => ss delsimps [@{thm split_paired_All}])) *})
 done
 
 lemma conforms_upd_local: