src/HOL/Tools/datatype_abs_proofs.ML

     val thy1 = add_path flat_names big_name thy;
 
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
 
-    val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
+    val size_name = Sign.intern_const (Theory.sign_of (theory "NatArith")) "size";
     val size_names = replicate (length (hd descr)) size_name @
       map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
         (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
     val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
       (map (fn T => name_of_typ T ^ "_size") recTs));