src/HOL/Basic_BNF_Least_Fixpoints.thy

--- a/src/HOL/Basic_BNF_Least_Fixpoints.thy	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy	Fri Sep 19 13:27:04 2014 +0200
@@ -55,11 +55,7 @@
 
 ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
 
-thm sum.rec_o_map
-thm sum.size_o_map
-
-thm prod.rec_o_map
-thm prod.size_o_map
+ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
 
 hide_const (open) xtor ctor_rec