Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Alternative names are now also used when storing theorems for
authorberghofe
Tue, 18 Dec 2007 12:26:00 +0100
changeset 25689 4853eeb03158
parent 25688 6c24a82a98f1
child 25690 5226396bf261
Alternative names are now also used when storing theorems for size functions.
src/HOL/Tools/function_package/size.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle