1.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports ExecutableContent Code_Char Efficient_Nat
     1.5  begin
     1.6  
     1.7 -declare isnorm.simps [code func del]
     1.8 +declare isnorm.simps [code del]
     1.9  
    1.10  ML {* (*FIXME get rid of this*)
    1.11  nonfix union;