1.1 --- a/src/HOL/Wellfounded.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4       (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
     1.5  
     1.6    wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
     1.7 -  [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
     1.8 +  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
     1.9  
    1.10  abbreviation acyclicP :: "('a => 'a => bool) => bool" where
    1.11    "acyclicP r == acyclic {(x, y). r x y}"
    1.12 @@ -840,10 +840,10 @@
    1.13  
    1.14  setup Size.setup
    1.15  
    1.16 -lemma size_bool [code func]:
    1.17 +lemma size_bool [code]:
    1.18    "size (b\<Colon>bool) = 0" by (cases b) auto
    1.19  
    1.20 -lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
    1.21 +lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
    1.22    by (induct n) simp_all
    1.23  
    1.24  declare "prod.size" [noatp]