src/HOL/Tools/datatype_prop.ML
changeset 10212 33fe2d701ddd
parent 9739 8470c4662685
child 10214 77349ed89f45
--- a/src/HOL/Tools/datatype_prop.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Thu Oct 12 18:38:23 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 "Arith")) "size";
+    val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "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))));