--- 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
--- a/src/HOL/Code_Numeral.thy Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Code_Numeral.thy Fri Sep 19 13:27:04 2014 +0200
@@ -809,15 +809,19 @@
shows P
using assms by transfer blast
-instantiation natural :: size
-begin
+lemma [simp, code]: "size_natural = nat_of_natural"
+proof (rule ext)
+ fix n
+ show "size_natural n = nat_of_natural n"
+ by (induct n) simp_all
+qed
-definition size_natural :: "natural \<Rightarrow> nat" where
- [simp, code]: "size_natural = nat_of_natural"
-
-instance ..
-
-end
+lemma [simp, code]: "size = nat_of_natural"
+proof (rule ext)
+ fix n
+ show "size n = nat_of_natural n"
+ by (induct n) simp_all
+qed
lemma natural_decr [termination_simp]:
"n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
--- a/src/HOL/Library/Old_Datatype.thy Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Library/Old_Datatype.thy Fri Sep 19 13:27:04 2014 +0200
@@ -10,7 +10,6 @@
keywords "old_datatype" :: thy_decl
begin
-ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
ML_file "~~/src/HOL/Tools/datatype_realizer.ML"