Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/datatype_package.ML
changeset 30280 eb98b49ef835
parent 30248 4f699164ab0c
child 30345 76fd85bbf139 
--- a/src/HOL/Tools/datatype_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -174,9 +174,9 @@
 
 fun dt_cases (descr: descr) (_, args, constrs) =
   let
-    fun the_bname i = Sign.base_name (#1 (the (AList.lookup (op =) descr i)));
+    fun the_bname i = NameSpace.base_name (#1 (the (AList.lookup (op =) descr i)));
     val bnames = map the_bname (distinct (op =) (maps dt_recs args));
-  in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
+  in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
 
 
 fun induct_cases descr =
@@ -519,7 +519,7 @@
     val cs = map (apsnd (map norm_constr)) raw_cs;
     val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
       o fst o strip_type;
-    val new_type_names = map NameSpace.base (the_default (map fst cs) alt_names);
+    val new_type_names = map NameSpace.base_name (the_default (map fst cs) alt_names);
 
     fun mk_spec (i, (tyco, constr)) = (i, (tyco,
       map (DtTFree o fst) vs,
isabelle