diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/MicroJava/J/Conform.thy
--- 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: