# HG changeset patch
# User wenzelm
# Date 1215811045 -7200
# Node ID dfda3192dec29c8ef2456e73289b41e5fde15c20
# Parent  2deaa546ba0d876c3fcf87015144f8e2267f6c81
Sorts.weaken: abstract argument;
tuned;

diff -r 2deaa546ba0d -r dfda3192dec2 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Fri Jul 11 23:17:23 2008 +0200
+++ b/src/Pure/sorts.ML	Fri Jul 11 23:17:25 2008 +0200
@@ -52,7 +52,7 @@
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   val meet_sort: algebra -> typ * sort -> sort Vartab.table -> sort Vartab.table
   val of_sort: algebra -> typ * sort -> bool
-  val weaken: 'b Graph.T -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a;
+  val weaken: algebra -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a
   val of_sort_derivation: Pretty.pp -> algebra ->
     {class_relation: 'a * class -> class -> 'a,
      type_constructor: string -> ('a * class) list list -> class -> 'a,
@@ -371,19 +371,20 @@
 
 (* animating derivations *)
 
-fun weaken classes class_relation (x, c1) c2 =
-  (case Graph.irreducible_paths classes (c1, c2) of
-    [] => raise CLASS_ERROR (NoClassrel (c1, c2))
-    | cs :: _ => let
-        fun weaken_path (x, c1 :: c2 :: cs) =
-            weaken_path (class_relation (x, c1) c2, c2 :: cs)
-          | weaken_path (x, _) = x;
-      in weaken_path (x, cs) end);
+fun weaken algebra class_relation =
+  let
+    fun path (x, c1 :: c2 :: cs) = path (class_relation (x, c1) c2, c2 :: cs)
+      | path (x, _) = x;
+  in fn (x, c1) => fn c2 =>
+    (case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
+      [] => raise CLASS_ERROR (NoClassrel (c1, c2))
+    | cs :: _ => path (x, cs))
+  end;
 
 fun of_sort_derivation pp algebra {class_relation, type_constructor, type_variable} =
   let
-    val {classes, arities} = rep_algebra algebra;
-    val weaken = weaken classes class_relation;
+    val weaken = weaken algebra class_relation;
+    val arities = arities_of algebra;
 
     fun weakens S1 S2 = S2 |> map (fn c2 =>
       (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of