removed dead code;
Sorts.of_sort_derivation: removed unused pp;

--- a/src/Pure/axclass.ML	Wed Sep 30 22:31:16 2009 +0200
+++ b/src/Pure/axclass.ML	Wed Sep 30 22:53:33 2009 +0200
@@ -150,7 +150,6 @@
   let val params = #2 (get_axclasses thy);
   in fold (fn (x, c) => if pred c then cons x else I) params [] end;
 
-fun params_of thy c = get_params thy (fn c' => c' = c);
 fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
 
 fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
@@ -263,7 +262,8 @@
 
 fun unoverload_const thy (c_ty as (c, _)) =
   case class_of_param thy c
-   of SOME class => (case get_inst_tyco (Sign.consts_of thy) c_ty
+   of SOME class (* FIXME unused? *) =>
+     (case get_inst_tyco (Sign.consts_of thy) c_ty
        of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
         | NONE => c)
     | NONE => c;
@@ -585,7 +585,7 @@
         val hyps = vars
           |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
         val ths = (typ, sort)
-          |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
+          |> Sorts.of_sort_derivation (Sign.classes_of thy)
            {class_relation =
               fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
             type_constructor =

--- a/src/Pure/sorts.ML	Wed Sep 30 22:31:16 2009 +0200
+++ b/src/Pure/sorts.ML	Wed Sep 30 22:53:33 2009 +0200
@@ -57,7 +57,7 @@
   val meet_sort_typ: algebra -> typ * sort -> typ -> typ   (*exception CLASS_ERROR*)
   val of_sort: algebra -> typ * sort -> bool
   val weaken: algebra -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a
-  val of_sort_derivation: Pretty.pp -> algebra ->
+  val of_sort_derivation: algebra ->
     {class_relation: 'a * class -> class -> 'a,
      type_constructor: string -> ('a * class) list list -> class -> 'a,
      type_variable: typ -> ('a * class) list} ->
@@ -401,7 +401,7 @@
     | cs :: _ => path (x, cs))
   end;
 
-fun of_sort_derivation pp algebra {class_relation, type_constructor, type_variable} =
+fun of_sort_derivation algebra {class_relation, type_constructor, type_variable} =
   let
     val weaken = weaken algebra class_relation;
     val arities = arities_of algebra;