1.1 --- a/src/Tools/code/code_target.ML	Mon May 04 14:49:50 2009 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Mon May 04 14:49:51 2009 +0200
     1.3 @@ -326,7 +326,7 @@
     1.4  fun add_module_alias target (thyname, modlname) =
     1.5    let
     1.6      val xs = Long_Name.explode modlname;
     1.7 -    val xs' = map (Code_Name.purify_name true) xs;
     1.8 +    val xs' = map (Name.desymbolize true) xs;
     1.9    in if xs' = xs
    1.10      then map_module_alias target (Symtab.update (thyname, modlname))
    1.11      else error ("Invalid module name: " ^ quote modlname ^ "\n"
    1.12 @@ -502,7 +502,7 @@
    1.13  
    1.14  fun read_const_exprs thy cs =
    1.15    let
    1.16 -    val (cs1, cs2) = Code_Name.read_const_exprs thy cs;
    1.17 +    val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
    1.18      val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
    1.19      val names4 = transitivly_non_empty_funs thy naming program;
    1.20      val cs5 = map_filter