1.1 --- a/src/HOL/Word/Word.thy	Wed Aug 27 15:55:01 2014 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Thu Aug 28 00:40:19 2014 +0200
     1.3 @@ -137,11 +137,11 @@
     1.4  definition source_size :: "('a::len0 word \<Rightarrow> 'b) \<Rightarrow> nat"
     1.5  where
     1.6    -- "whether a cast (or other) function is to a longer or shorter length"
     1.7 -  "source_size c = (let arb = undefined ; x = c arb in size arb)"  
     1.8 +  [code del]: "source_size c = (let arb = undefined; x = c arb in size arb)"
     1.9  
    1.10  definition target_size :: "('a \<Rightarrow> 'b::len0 word) \<Rightarrow> nat"
    1.11  where
    1.12 -  "target_size c = size (c undefined)"
    1.13 +  [code del]: "target_size c = size (c undefined)"
    1.14  
    1.15  definition is_up :: "('a::len0 word \<Rightarrow> 'b::len0 word) \<Rightarrow> bool"
    1.16  where