# HG changeset patch
# User blanchet
# Date 1411126024 -7200
# Node ID b74d8470b98e0b0c76fcaaeab2fe00c68da748ac
# Parent  ee1f45ca0d73fe0f706f87e28959fe8620d06211
keep obsolete interpretations in Main, to avoid merge trouble

diff -r ee1f45ca0d73 -r b74d8470b98e 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
 
diff -r ee1f45ca0d73 -r b74d8470b98e src/HOL/Code_Numeral.thy
--- 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"
diff -r ee1f45ca0d73 -r b74d8470b98e src/HOL/Library/Old_Datatype.thy
--- 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"