src/HOL/Tools/datatype_abs_proofs.ML
changeset 10212 33fe2d701ddd
parent 9969 4753185f1dd2
child 10214 77349ed89f45
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 12 18:09:06 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 12 18:38:23 2000 +0200
     1.3 @@ -417,7 +417,7 @@
     1.4      val descr' = flat descr;
     1.5      val recTs = get_rec_types descr' sorts;
     1.6  
     1.7 -    val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
     1.8 +    val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
     1.9      val size_names = replicate (length (hd descr)) size_name @
    1.10        map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
    1.11          (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));