# HG changeset patch
# User blanchet
# Date 1409179219 -7200
# Node ID decb3e2528e7a1b80827505b4ad774bb6be773c5
# Parent  ec66337a7162f48c4dbe71be4391512369e17267
removed needless, and for (newer versions of?) Haskell problematic code equations

diff -r ec66337a7162 -r decb3e2528e7 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Aug 27 15:55:01 2014 +0200
+++ b/src/HOL/Word/Word.thy	Thu Aug 28 00:40:19 2014 +0200
@@ -137,11 +137,11 @@
 definition source_size :: "('a::len0 word \<Rightarrow> 'b) \<Rightarrow> nat"
 where
   -- "whether a cast (or other) function is to a longer or shorter length"
-  "source_size c = (let arb = undefined ; x = c arb in size arb)"  
+  [code del]: "source_size c = (let arb = undefined; x = c arb in size arb)"
 
 definition target_size :: "('a \<Rightarrow> 'b::len0 word) \<Rightarrow> nat"
 where
-  "target_size c = size (c undefined)"
+  [code del]: "target_size c = size (c undefined)"
 
 definition is_up :: "('a::len0 word \<Rightarrow> 'b::len0 word) \<Rightarrow> bool"
 where