src/Pure/sorts.ML
changeset 36104 fecb587a1d0e
parent 36103 b2b9b687a4c4
child 36105 42c37cf849cd
     1.1 --- a/src/Pure/sorts.ML	Sun Apr 11 13:13:23 2010 +0200
     1.2 +++ b/src/Pure/sorts.ML	Sun Apr 11 14:04:10 2010 +0200
     1.3 @@ -410,10 +410,15 @@
     1.4    let
     1.5      val arities = arities_of algebra;
     1.6  
     1.7 -    fun weaken T S1 S2 = S2 |> map (fn c2 =>
     1.8 -      (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
     1.9 -        SOME d1 => class_relation T d1 c2
    1.10 -      | NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
    1.11 +    fun weaken T D1 S2 =
    1.12 +      let val S1 = map snd D1 in
    1.13 +        if S1 = S2 then map fst D1
    1.14 +        else
    1.15 +          S2 |> map (fn c2 =>
    1.16 +            (case D1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
    1.17 +              SOME d1 => class_relation T d1 c2
    1.18 +            | NONE => raise CLASS_ERROR (NoSubsort (S1, S2))))
    1.19 +      end;
    1.20  
    1.21      fun derive (_, []) = []
    1.22        | derive (T as Type (a, Us), S) =