1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Oct 19 09:11:18 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Oct 19 09:11:18 2011 +0200
     1.3 @@ -268,15 +268,17 @@
     1.4  (* policies *)
     1.5  
     1.6  local
     1.7 +  fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
     1.8    fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
     1.9 +  fun thyname_of_const' thy = #theory_name o Name_Space.the_entry (Sign.const_space thy);
    1.10    fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst
    1.11     of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
    1.12      | thyname :: _ => thyname;
    1.13    fun thyname_of_const thy c = case AxClass.class_of_param thy c
    1.14     of SOME class => thyname_of_class thy class
    1.15      | NONE => (case Code.get_type_of_constr_or_abstr thy c
    1.16 -       of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
    1.17 -        | NONE => Codegen.thyname_of_const thy c);
    1.18 +       of SOME (tyco, _) => thyname_of_type thy tyco
    1.19 +        | NONE => thyname_of_const' thy c);
    1.20    fun purify_base "==>" = "follows"
    1.21      | purify_base "==" = "meta_eq"
    1.22      | purify_base s = Name.desymbolize false s;
    1.23 @@ -293,7 +295,7 @@
    1.24    (fn thy => thyname_of_class thy o fst);
    1.25    (*order fits nicely with composed projections*)
    1.26  fun namify_tyco thy "fun" = "Pure.fun"
    1.27 -  | namify_tyco thy tyco = namify thy Long_Name.base_name Codegen.thyname_of_type tyco;
    1.28 +  | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_type tyco;
    1.29  fun namify_instance thy = namify thy (fn (class, tyco) => 
    1.30    Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
    1.31  fun namify_const thy = namify thy Long_Name.base_name thyname_of_const;