src/HOL/MicroJava/J/Conform.thy

 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_local (fn ss => ss delsimps [@{thm split_paired_All}])) *})
+    |> map_simpset (fn ss => ss delsimps [@{thm split_paired_All}])) *})
 done
 
 lemma conforms_upd_local: 
 "[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] 
   ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)"