src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Tue Jan 02 23:04:15 2018 +0100
+++ b/src/HOL/Nat.thy	Wed Jan 03 11:06:13 2018 +0100
@@ -2456,6 +2456,8 @@
 
 end
 
+lemmas size_nat = size_nat_def
+
 
 subsection \<open>Code module namespace\<close>