Sorts.minimal_classes;
authorwenzelm
Fri Dec 29 17:24:45 2006 +0100 (2006-12-29)
changeset 21934ba683b0b2456
parent 21933 819ef284720b
child 21935 4e20a5397b57
Sorts.minimal_classes;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Fri Dec 29 17:24:44 2006 +0100
     1.2 +++ b/src/Pure/type.ML	Fri Dec 29 17:24:45 2006 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4        Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
     1.5        |> Library.sort (Library.int_ord o pairself snd) |> map fst;
     1.6      val witness =
     1.7 -      (case Sorts.witness_sorts classes log_types [] [Sorts.classes classes] of
     1.8 +      (case Sorts.witness_sorts classes log_types [] [Sorts.minimal_classes classes] of
     1.9          [w] => SOME w | _ => NONE);
    1.10    in make_tsig ((space, classes), default, types, log_types, witness) end;
    1.11