# HG changeset patch
# User wenzelm
# Date 1270987450 -7200
# Node ID fecb587a1d0e20944e3579f8c9e4be08ad5e1d6e
# Parent  b2b9b687a4c411e5a72c9478cb6e8639d70ce12d
of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;

diff -r b2b9b687a4c4 -r fecb587a1d0e src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sun Apr 11 13:13:23 2010 +0200
+++ b/src/Pure/sorts.ML	Sun Apr 11 14:04:10 2010 +0200
@@ -410,10 +410,15 @@
   let
     val arities = arities_of algebra;
 
-    fun weaken T S1 S2 = S2 |> map (fn c2 =>
-      (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
-        SOME d1 => class_relation T d1 c2
-      | NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
+    fun weaken T D1 S2 =
+      let val S1 = map snd D1 in
+        if S1 = S2 then map fst D1
+        else
+          S2 |> map (fn c2 =>
+            (case D1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
+              SOME d1 => class_relation T d1 c2
+            | NONE => raise CLASS_ERROR (NoSubsort (S1, S2))))
+      end;
 
     fun derive (_, []) = []
       | derive (T as Type (a, Us), S) =