1.1 --- a/src/HOL/Bali/Example.thy	Fri May 15 10:01:57 2009 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Sat May 16 11:28:02 2009 +0200
     1.3 @@ -1075,10 +1075,7 @@
     1.4  lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = 
     1.5    {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
     1.6     , [Class Base])}"
     1.7 -apply (unfold max_spec_def)
     1.8 -apply (simp (no_asm) add: appl_methds_Base_foo)
     1.9 -apply auto
    1.10 -done
    1.11 +by (simp (no_asm) add: max_spec_def appl_methds_Base_foo)
    1.12  
    1.13  section "well-typedness"
    1.14