# HG changeset patch
# User haftmann
# Date 1235161774 -3600
# Node ID 00d04a562df1a3784716263cdf2e9eaa6a9105e5
# Parent  f2421131a83cc39cd16ef13326eafc37dd387a87# Parent  d14d0b4bf5b466c46491e7ea0a5b341fcaed6e75
merged

diff -r f2421131a83c -r 00d04a562df1 src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Fri Feb 20 20:51:06 2009 +0100
+++ b/src/Tools/code/code_wellsorted.ML	Fri Feb 20 21:29:34 2009 +0100
@@ -50,9 +50,9 @@
 fun complete_proper_sort thy =
   Sign.complete_sort thy #> filter (can (AxClass.get_info thy));
 
-fun inst_params thy tyco class =
+fun inst_params thy tyco =
   map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
-    ((#params o AxClass.get_info thy) class);
+    o maps (#params o AxClass.get_info thy);
 
 fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
   (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
@@ -100,12 +100,11 @@
   case AList.lookup (op =) arities inst
    of SOME classess => (classess, ([], []))
     | NONE => let
+        val all_classes = complete_proper_sort thy [class];
+        val superclasses = remove (op =) class all_classes
         val classess = map (complete_proper_sort thy)
           (Sign.arity_sorts thy tyco [class]);
-        val superclasses = [class]
-          |> complete_proper_sort thy
-          |> remove (op =) class;
-        val inst_params = inst_params thy tyco class;
+        val inst_params = inst_params thy tyco all_classes;
       in (classess, (superclasses, inst_params)) end;
 
 fun add_classes thy arities eqngr c_k new_classes vardeps_data =
@@ -225,7 +224,7 @@
   let
     fun class_relation (x, _) _ = x;
     fun type_constructor tyco xs class =
-      inst_params thy tyco class @ (maps o maps) fst xs;
+      inst_params thy tyco (Sorts.complete_sort algebra [class]) @ (maps o maps) fst xs;
     fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
   in
     flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra