# HG changeset patch
# User wenzelm
# Date 1429184361 -7200
# Node ID 20d437414174c4a4812a66e8ec9fd299eefdfd5d
# Parent  9feddd64183eb47e95614e47c28bce4edf1605e3
tuned;

diff -r 9feddd64183e -r 20d437414174 src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Thu Apr 16 12:37:30 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML	Thu Apr 16 13:39:21 2015 +0200
@@ -6,31 +6,30 @@
 
 signature CLASS_DEPS =
 sig
-  val class_deps: Proof.context -> sort list option * sort list option ->
-    Graph_Display.entry list
+  val class_deps: Proof.context -> sort list option * sort list option -> Graph_Display.entry list
   val class_deps_cmd: Proof.context -> string list option * string list option -> unit
 end;
 
 structure Class_Deps: CLASS_DEPS =
 struct
 
-fun gen_class_deps prep_sort ctxt raw_bounds =
+fun gen_class_deps prep_sort ctxt bounds =
   let
-    val (upper, lower) = apply2 ((Option.map o map) (prep_sort ctxt)) raw_bounds;
+    val (upper, lower) = apply2 ((Option.map o map) (prep_sort ctxt)) bounds;
     val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
-    val sort_le = curry (Sorts.sort_le algebra);
-    val restrict =
+    val rel = Sorts.sort_le algebra;
+    val pred =
       (case upper of
-        SOME bs => (fn c => exists (fn b => sort_le [c] b) bs)
+        SOME bs => (fn c => exists (fn b => rel ([c], b)) bs)
       | NONE => K true) andf
       (case lower of
-        SOME bs => (fn c => exists (fn b => sort_le b [c]) bs)
+        SOME bs => (fn c => exists (fn b => rel (b, [c])) bs)
       | NONE => K true);
     fun node c =
       Graph_Display.content_node (Name_Space.extern ctxt space c)
         (Class.pretty_specification (Proof_Context.theory_of ctxt) c);
   in
-    Sorts.subalgebra (Context.pretty ctxt) restrict (K NONE) algebra
+    Sorts.subalgebra (Context.pretty ctxt) pred (K NONE) algebra
     |> #2 |> Sorts.classes_of |> Graph.dest
     |> map (fn ((c, _), ds) => ((c, node c), ds))
   end;