1.1 --- a/src/HOL/MicroJava/J/Conform.thy	Wed May 26 16:28:55 2010 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Wed May 26 16:31:44 2010 +0200
     1.3 @@ -328,8 +328,8 @@
     1.4  apply  auto
     1.5  apply(rule hconfI)
     1.6  apply(drule conforms_heapD)
     1.7 -apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] 
     1.8 -                addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *})
     1.9 +apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}] 
    1.10 +                addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *})
    1.11  done
    1.12  
    1.13  lemma conforms_upd_local: 

     2.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Wed May 26 16:28:55 2010 +0200
     2.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Wed May 26 16:31:44 2010 +0200
     2.3 @@ -228,7 +228,7 @@
     2.4        EVERY [
     2.5          REPEAT (etac thin_rl i),
     2.6          cut_facts_tac (mk_lam_defs defs) i,
     2.7 -        full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
     2.8 +        full_simp_tac (Mucke_ss delsimps [not_iff, @{thm split_part}]) i,
     2.9          move_mus i, call_mucke_tac i,atac i,
    2.10          REPEAT (rtac refl i)] state);
    2.11  *}