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