src/HOL/Tools/datatype_package.ML
changeset 30364 577edc39b501
parent 30345 76fd85bbf139
child 30391 d930432adb13
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -174,9 +174,9 @@
     1.4  
     1.5  fun dt_cases (descr: descr) (_, args, constrs) =
     1.6    let
     1.7 -    fun the_bname i = NameSpace.base_name (#1 (the (AList.lookup (op =) descr i)));
     1.8 +    fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
     1.9      val bnames = map the_bname (distinct (op =) (maps dt_recs args));
    1.10 -  in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
    1.11 +  in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
    1.12  
    1.13  
    1.14  fun induct_cases descr =
    1.15 @@ -519,7 +519,7 @@
    1.16      val cs = map (apsnd (map norm_constr)) raw_cs;
    1.17      val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
    1.18        o fst o strip_type;
    1.19 -    val new_type_names = map NameSpace.base_name (the_default (map fst cs) alt_names);
    1.20 +    val new_type_names = map Long_Name.base_name (the_default (map fst cs) alt_names);
    1.21  
    1.22      fun mk_spec (i, (tyco, constr)) = (i, (tyco,
    1.23        map (DtTFree o fst) vs,