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: