1.1 --- a/src/Pure/Isar/class_target.ML	Tue Apr 28 13:34:48 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Tue Apr 28 13:34:48 2009 +0200
     1.3 @@ -278,7 +278,8 @@
     1.4      val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
     1.5        (K tac);
     1.6      val diff_sort = Sign.complete_sort thy [sup]
     1.7 -      |> subtract (op =) (Sign.complete_sort thy [sub]);
     1.8 +      |> subtract (op =) (Sign.complete_sort thy [sub])
     1.9 +      |> filter (is_class thy);
    1.10    in
    1.11      thy
    1.12      |> AxClass.add_classrel classrel