# HG changeset patch
# User haftmann
# Date 1240918488 -7200
# Node ID 751f5aa3e3153c53aa3d07cb117d582dd339ecd8
# Parent  506e57123cd18f3d553f5dbe307f86544d91556f
prevent potential failure

diff -r 506e57123cd1 -r 751f5aa3e315 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Tue Apr 28 13:34:48 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Tue Apr 28 13:34:48 2009 +0200
@@ -278,7 +278,8 @@
     val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
       (K tac);
     val diff_sort = Sign.complete_sort thy [sup]
-      |> subtract (op =) (Sign.complete_sort thy [sub]);
+      |> subtract (op =) (Sign.complete_sort thy [sub])
+      |> filter (is_class thy);
   in
     thy
     |> AxClass.add_classrel classrel