removed obsolete AxClass.params_of_class;
authorwenzelm
Thu Oct 11 16:05:47 2007 +0200 (2007-10-11)
changeset 24969b38527eefb3b
parent 24968 f9bafc868847
child 24970 050afeec89a7
removed obsolete AxClass.params_of_class;
tuned;
src/Pure/Isar/code.ML
src/Tools/code/code_funcgr.ML
src/Tools/code/code_thingol.ML
     1.1 --- a/src/Pure/Isar/code.ML	Thu Oct 11 16:05:44 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 11 16:05:47 2007 +0200
     1.3 @@ -545,8 +545,7 @@
     1.4  fun specific_constraints thy (class, tyco) =
     1.5    let
     1.6      val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
     1.7 -    val classparams = (map fst o these o Option.map snd
     1.8 -      o try (AxClass.params_of_class thy)) class;
     1.9 +    val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
    1.10      val funcs = classparams
    1.11        |> map (fn c => Class.inst_const thy (c, tyco))
    1.12        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
    1.13 @@ -579,9 +578,9 @@
    1.14  
    1.15  fun gen_classparam_typ constr thy class (c, tyco) = 
    1.16    let
    1.17 -    val (var, cs) = try (AxClass.params_of_class thy) class |> the_default (Name.aT, [])
    1.18 +    val cs = these (try (#params o AxClass.get_info thy) class);
    1.19      val ty = (the o AList.lookup (op =) cs) c;
    1.20 -    val sort_args = Name.names (Name.declare var Name.context) Name.aT
    1.21 +    val sort_args = Name.names (Name.declare Name.aT Name.context) Name.aT
    1.22        (constr thy (class, tyco));
    1.23      val ty_inst = Type (tyco, map TFree sort_args);
    1.24    in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;
     2.1 --- a/src/Tools/code/code_funcgr.ML	Thu Oct 11 16:05:44 2007 +0200
     2.2 +++ b/src/Tools/code/code_funcgr.ML	Thu Oct 11 16:05:47 2007 +0200
     2.3 @@ -156,9 +156,7 @@
     2.4    let
     2.5      val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
     2.6      fun all_classparams tyco class =
     2.7 -      try (AxClass.params_of_class thy) class
     2.8 -      |> Option.map snd
     2.9 -      |> these
    2.10 +      these (try (#params o AxClass.get_info thy) class)
    2.11        |> map (fn (c, _) => Class.inst_const thy (c, tyco))
    2.12    in
    2.13      Symtab.empty
     3.1 --- a/src/Tools/code/code_thingol.ML	Thu Oct 11 16:05:44 2007 +0200
     3.2 +++ b/src/Tools/code/code_thingol.ML	Thu Oct 11 16:05:47 2007 +0200
     3.3 @@ -346,14 +346,14 @@
     3.4  fun ensure_class thy (algbr as ((_, algebra), _)) funcgr class =
     3.5    let
     3.6      val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
     3.7 -    val (v, cs) = AxClass.params_of_class thy class;
     3.8 +    val cs = #params (AxClass.get_info thy class);
     3.9      val class' = CodeName.class thy class;
    3.10      val stmt_class =
    3.11        fold_map (fn superclass => ensure_class thy algbr funcgr superclass
    3.12          ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
    3.13        ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
    3.14          ##>> exprgen_typ thy algbr funcgr ty) cs
    3.15 -      #>> (fn info => Class (unprefix "'" v, info))
    3.16 +      #>> (fn info => Class (unprefix "'" Name.aT, info))
    3.17    in
    3.18      ensure_stmt stmt_class class'
    3.19    end
    3.20 @@ -445,7 +445,7 @@
    3.21  and ensure_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
    3.22    let
    3.23      val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
    3.24 -    val (var, classparams) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
    3.25 +    val classparams = these (try (#params o AxClass.get_info thy) class);
    3.26      val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
    3.27      val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
    3.28      val vs' = map2 (fn (v, sort1) => fn sort2 => (v,