src/Tools/Code/code_thingol.ML
changeset 33172 61ee96bc9895
parent 33029 2fefe039edf1
child 33187 616be6d7997e
     1.1 --- a/src/Tools/Code/code_thingol.ML	Sun Oct 25 19:21:34 2009 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Sun Oct 25 20:54:21 2009 +0100
     1.3 @@ -252,19 +252,15 @@
     1.4  (* policies *)
     1.5  
     1.6  local
     1.7 -  fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
     1.8 -  fun thyname_of_class thy =
     1.9 -    thyname_of thy (ProofContext.query_class (ProofContext.init thy));
    1.10 -  fun thyname_of_tyco thy =
    1.11 -    thyname_of thy (Type.the_tags (Sign.tsig_of thy));
    1.12 -  fun thyname_of_instance thy inst = case AxClass.arity_property thy inst Markup.theory_nameN
    1.13 -   of [] => error ("no such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
    1.14 +  fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
    1.15 +  fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst
    1.16 +   of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
    1.17      | thyname :: _ => thyname;
    1.18    fun thyname_of_const thy c = case AxClass.class_of_param thy c
    1.19     of SOME class => thyname_of_class thy class
    1.20      | NONE => (case Code.get_datatype_of_constr thy c
    1.21 -       of SOME dtco => thyname_of_tyco thy dtco
    1.22 -        | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c);
    1.23 +       of SOME dtco => Codegen.thyname_of_type thy dtco
    1.24 +        | NONE => Codegen.thyname_of_const thy c);
    1.25    fun purify_base "op &" = "and"
    1.26      | purify_base "op |" = "or"
    1.27      | purify_base "op -->" = "implies"
    1.28 @@ -282,10 +278,11 @@
    1.29  
    1.30  fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
    1.31  fun namify_classrel thy = namify thy (fn (class1, class2) => 
    1.32 -  Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1) (fn thy => thyname_of_class thy o fst);
    1.33 +    Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1)
    1.34 +  (fn thy => thyname_of_class thy o fst);
    1.35    (*order fits nicely with composed projections*)
    1.36  fun namify_tyco thy "fun" = "Pure.fun"
    1.37 -  | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_tyco tyco;
    1.38 +  | namify_tyco thy tyco = namify thy Long_Name.base_name Codegen.thyname_of_type tyco;
    1.39  fun namify_instance thy = namify thy (fn (class, tyco) => 
    1.40    Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
    1.41  fun namify_const thy = namify thy Long_Name.base_name thyname_of_const;