# HG changeset patch
# User berghofe
# Date 1197977160 -3600
# Node ID 4853eeb031584eb6371e3b8933eb172e51d27619
# Parent  6c24a82a98f16644a9e1cf0ea3133ed23268e249
Alternative names are now also used when storing theorems for
size functions.

diff -r 6c24a82a98f1 -r 4853eeb03158 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Tue Dec 18 11:45:08 2007 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Tue Dec 18 12:26:00 2007 +0100
@@ -215,9 +215,9 @@
 
 fun add_size_thms (new_type_names as name :: _) thy =
   let
-    val info as {descr, ...} = DatatypePackage.the_datatype thy name;
-    val prefix = NameSpace.map_base
-      (K (space_implode "_" (map Sign.base_name new_type_names))) name;
+    val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
+    val prefix = NameSpace.map_base (K (space_implode "_"
+      (the_default (map Sign.base_name new_type_names) alt_names))) name;
     val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
       is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr
   in if no_size then thy