# HG changeset patch
# User berghofe
# Date 967636497 -7200
# Node ID 8470c4662685503ae748d15ead8a8d9ea6352b77
# Parent  2e1dca5af2d4f674deb68baac7d228fd41ea17cf
Improved names for size function.

diff -r 2e1dca5af2d4 -r 8470c4662685 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Aug 30 13:54:53 2000 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Aug 30 13:54:57 2000 +0200
@@ -417,15 +417,12 @@
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
 
-    val big_size_name = space_implode "_" new_type_names ^ "_size";
     val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
     val size_names = replicate (length (hd descr)) size_name @
-      map (Sign.full_name (Theory.sign_of thy1))
-        (if length (flat (tl descr)) = 1 then [big_size_name] else
-          map (fn i => big_size_name ^ "_" ^ string_of_int i)
-            (1 upto length (flat (tl descr))));
-    val def_names = map (fn i => big_size_name ^ "_def_" ^ string_of_int i)
-      (1 upto length recTs);
+      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));
 
     fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
 
@@ -456,7 +453,7 @@
 
     val size_thms = map (fn t => prove_goalw_cterm rewrites
       (cterm_of (Theory.sign_of thy') t) (fn _ => [rtac refl 1]))
-        (DatatypeProp.make_size new_type_names descr sorts thy')
+        (DatatypeProp.make_size descr sorts thy')
 
   in
     thy' |> Theory.add_path big_name |>
diff -r 2e1dca5af2d4 -r 8470c4662685 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Aug 30 13:54:53 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Aug 30 13:54:57 2000 +0200
@@ -456,10 +456,8 @@
       (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
         (1 upto (length descr')));
 
-    val big_size_name = space_implode "_" new_type_names ^ "_size";
-    val size_names = if length (flat (tl descr)) = 1 then [big_size_name] else
-      map (fn i => big_size_name ^ "_" ^ string_of_int i)
-        (1 upto length (flat (tl descr)));
+    val size_names = DatatypeProp.indexify_names
+      (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs)));
 
     val freeT = TFree (variant used "'t", HOLogic.termS);
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
@@ -517,7 +515,7 @@
     (**** introduction of axioms ****)
 
     val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
-    val size_axs = if no_size then [] else DatatypeProp.make_size new_type_names descr sorts thy2;
+    val size_axs = if no_size then [] else DatatypeProp.make_size descr sorts thy2;
 
     val (thy3, (([induct], [rec_thms]), inject)) =
       thy2 |>
diff -r 2e1dca5af2d4 -r 8470c4662685 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Wed Aug 30 13:54:53 2000 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Wed Aug 30 13:54:57 2000 +0200
@@ -31,7 +31,7 @@
       theory -> (term * term) list
   val make_case_trrules : string list -> (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> ast Syntax.trrule list
-  val make_size : string list -> (int * (string * DatatypeAux.dtyp list *
+  val make_size : (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       theory -> term list
   val make_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
@@ -393,18 +393,15 @@
 
 (******************************* size functions *******************************)
 
-fun make_size new_type_names descr sorts thy =
+fun make_size descr sorts thy =
   let
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
 
-    val big_size_name = space_implode "_" new_type_names ^ "_size";
     val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
     val size_names = replicate (length (hd descr)) size_name @
-      map (Sign.intern_const (Theory.sign_of thy))
-        (if length (flat (tl descr)) = 1 then [big_size_name] else
-          map (fn i => big_size_name ^ "_" ^ string_of_int i)
-            (1 upto length (flat (tl descr))));
+      map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
+        (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
     val size_consts = map (fn (s, T) =>
       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);