src/Tools/code/code_name.ML
changeset 30364 577edc39b501
parent 30161 c26e515f1c29
child 30648 17365ef082f3
     1.1 --- a/src/Tools/code/code_name.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Tools/code/code_name.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4  val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
     1.5  
     1.6  val dest_name =
     1.7 -  apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
     1.8 +  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
     1.9  
    1.10  
    1.11  (** purification **)
    1.12 @@ -80,7 +80,7 @@
    1.13    #> Symbol.scanner "Malformed name"
    1.14        (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
    1.15    #> implode
    1.16 -  #> NameSpace.explode
    1.17 +  #> Long_Name.explode
    1.18    #> map (purify_name true false);
    1.19  
    1.20  (*FIMXE non-canonical function treating non-canonical names*)
    1.21 @@ -101,11 +101,11 @@
    1.22  
    1.23  fun check_modulename mn =
    1.24    let
    1.25 -    val mns = NameSpace.explode mn;
    1.26 +    val mns = Long_Name.explode mn;
    1.27      val mns' = map (purify_name true false) mns;
    1.28    in
    1.29      if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
    1.30 -      ^ "perhaps try " ^ quote (NameSpace.implode mns'))
    1.31 +      ^ "perhaps try " ^ quote (Long_Name.implode mns'))
    1.32    end;
    1.33  
    1.34  
    1.35 @@ -155,11 +155,11 @@
    1.36      fun mk_alias name = case module_alias name
    1.37       of SOME name' => name'
    1.38        | NONE => name
    1.39 -          |> NameSpace.explode
    1.40 +          |> Long_Name.explode
    1.41            |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
    1.42 -          |> NameSpace.implode;
    1.43 +          |> Long_Name.implode;
    1.44      fun mk_prefix name = case module_prefix
    1.45 -     of SOME module_prefix => NameSpace.append module_prefix name
    1.46 +     of SOME module_prefix => Long_Name.append module_prefix name
    1.47        | NONE => name;
    1.48      val tab =
    1.49        Symtab.empty