diff -r 97d28302445c -r 50f9f699b2d7 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Fri Apr 20 22:48:48 2012 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Fri Apr 20 23:15:44 2012 +0200
@@ -137,7 +137,7 @@
 lemma NewCI: "[|new_Addr (heap s) = (a,x);  
        s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==>  
        G\<turnstile>Norm s -NewC C\<succ>Addr a-> s'"
-apply (simp (no_asm_simp))
+apply simp
 apply (rule eval_evals_exec.NewC)
 apply auto
 done
@@ -146,7 +146,7 @@
  "!!s s'. (G\<turnstile>(x,s) -e \<succ>  v -> (x',s') --> x'=None --> x=None) \<and>  
           (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x'=None --> x=None) \<and>  
           (G\<turnstile>(x,s) -c       -> (x',s') --> x'=None --> x=None)"
-apply(simp (no_asm_simp) only: split_tupled_all)
+apply(simp only: split_tupled_all)
 apply(rule eval_evals_exec_induct)
 apply(unfold c_hupd_def)
 apply(simp_all)
@@ -173,7 +173,7 @@
 "!!s s'. (G\<turnstile>(x,s) -e \<succ>  v -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and>  
          (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and>  
          (G\<turnstile>(x,s) -c       -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s)"
-apply (simp (no_asm_simp) only: split_tupled_all)
+apply (simp only: split_tupled_all)
 apply (rule eval_evals_exec_induct)
 apply (unfold c_hupd_def)
 apply (simp_all)