# HG changeset patch
# User wenzelm
# Date 1192111547 -7200
# Node ID b38527eefb3b15bef88fbbd9e0f1c4085b583e97
# Parent  f9bafc868847cad65d1204880ca41cf55b3ab423
removed obsolete AxClass.params_of_class;
tuned;

diff -r f9bafc868847 -r b38527eefb3b src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Oct 11 16:05:44 2007 +0200
+++ b/src/Pure/Isar/code.ML	Thu Oct 11 16:05:47 2007 +0200
@@ -545,8 +545,7 @@
 fun specific_constraints thy (class, tyco) =
   let
     val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
-    val classparams = (map fst o these o Option.map snd
-      o try (AxClass.params_of_class thy)) class;
+    val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
     val funcs = classparams
       |> map (fn c => Class.inst_const thy (c, tyco))
       |> map (Symtab.lookup ((the_funcs o the_exec) thy))
@@ -579,9 +578,9 @@
 
 fun gen_classparam_typ constr thy class (c, tyco) = 
   let
-    val (var, cs) = try (AxClass.params_of_class thy) class |> the_default (Name.aT, [])
+    val cs = these (try (#params o AxClass.get_info thy) class);
     val ty = (the o AList.lookup (op =) cs) c;
-    val sort_args = Name.names (Name.declare var Name.context) Name.aT
+    val sort_args = Name.names (Name.declare Name.aT Name.context) Name.aT
       (constr thy (class, tyco));
     val ty_inst = Type (tyco, map TFree sort_args);
   in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;
diff -r f9bafc868847 -r b38527eefb3b src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Thu Oct 11 16:05:44 2007 +0200
+++ b/src/Tools/code/code_funcgr.ML	Thu Oct 11 16:05:47 2007 +0200
@@ -156,9 +156,7 @@
   let
     val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
     fun all_classparams tyco class =
-      try (AxClass.params_of_class thy) class
-      |> Option.map snd
-      |> these
+      these (try (#params o AxClass.get_info thy) class)
       |> map (fn (c, _) => Class.inst_const thy (c, tyco))
   in
     Symtab.empty
diff -r f9bafc868847 -r b38527eefb3b src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Thu Oct 11 16:05:44 2007 +0200
+++ b/src/Tools/code/code_thingol.ML	Thu Oct 11 16:05:47 2007 +0200
@@ -346,14 +346,14 @@
 fun ensure_class thy (algbr as ((_, algebra), _)) funcgr class =
   let
     val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
-    val (v, cs) = AxClass.params_of_class thy class;
+    val cs = #params (AxClass.get_info thy class);
     val class' = CodeName.class thy class;
     val stmt_class =
       fold_map (fn superclass => ensure_class thy algbr funcgr superclass
         ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
       ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
         ##>> exprgen_typ thy algbr funcgr ty) cs
-      #>> (fn info => Class (unprefix "'" v, info))
+      #>> (fn info => Class (unprefix "'" Name.aT, info))
   in
     ensure_stmt stmt_class class'
   end
@@ -445,7 +445,7 @@
 and ensure_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
   let
     val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
-    val (var, classparams) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
+    val classparams = these (try (#params o AxClass.get_info thy) class);
     val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
     val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
     val vs' = map2 (fn (v, sort1) => fn sort2 => (v,