| changeset 42795 | 66fcc9882784 |
| parent 42793 | 88bee9f6eec7 |
| child 46206 | d3d62b528487 |
--- a/src/HOL/MicroJava/J/Conform.thy Fri May 13 23:24:06 2011 +0200 +++ b/src/HOL/MicroJava/J/Conform.thy Fri May 13 23:58:40 2011 +0200 @@ -330,7 +330,7 @@ apply(drule conforms_heapD) 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}])) *}) + |> map_simpset (fn ss => ss delsimps [@{thm split_paired_All}])) *}) done lemma conforms_upd_local: