src/HOL/Tools/datatype_prop.ML
changeset 10214 77349ed89f45
parent 10212 33fe2d701ddd
child 10911 eb5721204b38
--- a/src/HOL/Tools/datatype_prop.ML	Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Fri Oct 13 08:28:21 2000 +0200
@@ -398,7 +398,7 @@
     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.intern_const (Theory.sign_of thy)) (indexify_names
         (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));