src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -848,20 +848,6 @@
 done
 
 
-subsection {* size of a datatype value *}
-
-ML_file "Tools/Function/size.ML"
-setup Size.setup
-
-lemma size_bool [code]:
-  "size (b\<Colon>bool) = 0" by (cases b) auto
-
-lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
-  by (induct n) simp_all
-
-declare prod.size [no_atp]
-
-
 hide_const (open) acc accp
 
 end