1.1 --- a/src/Tools/code/code_wellsorted.ML	Fri Feb 20 20:51:06 2009 +0100
     1.2 +++ b/src/Tools/code/code_wellsorted.ML	Fri Feb 20 21:29:34 2009 +0100
     1.3 @@ -50,9 +50,9 @@
     1.4  fun complete_proper_sort thy =
     1.5    Sign.complete_sort thy #> filter (can (AxClass.get_info thy));
     1.6  
     1.7 -fun inst_params thy tyco class =
     1.8 +fun inst_params thy tyco =
     1.9    map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
    1.10 -    ((#params o AxClass.get_info thy) class);
    1.11 +    o maps (#params o AxClass.get_info thy);
    1.12  
    1.13  fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
    1.14    (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
    1.15 @@ -100,12 +100,11 @@
    1.16    case AList.lookup (op =) arities inst
    1.17     of SOME classess => (classess, ([], []))
    1.18      | NONE => let
    1.19 +        val all_classes = complete_proper_sort thy [class];
    1.20 +        val superclasses = remove (op =) class all_classes
    1.21          val classess = map (complete_proper_sort thy)
    1.22            (Sign.arity_sorts thy tyco [class]);
    1.23 -        val superclasses = [class]
    1.24 -          |> complete_proper_sort thy
    1.25 -          |> remove (op =) class;
    1.26 -        val inst_params = inst_params thy tyco class;
    1.27 +        val inst_params = inst_params thy tyco all_classes;
    1.28        in (classess, (superclasses, inst_params)) end;
    1.29  
    1.30  fun add_classes thy arities eqngr c_k new_classes vardeps_data =
    1.31 @@ -225,7 +224,7 @@
    1.32    let
    1.33      fun class_relation (x, _) _ = x;
    1.34      fun type_constructor tyco xs class =
    1.35 -      inst_params thy tyco class @ (maps o maps) fst xs;
    1.36 +      inst_params thy tyco (Sorts.complete_sort algebra [class]) @ (maps o maps) fst xs;
    1.37      fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
    1.38    in
    1.39      flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra