src/Pure/Isar/class_target.ML

         (fst o rules thy) sub];
     val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
     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
     |> ClassData.map (Graph.add_edge (sub, sup))
     |> activate_defs sub (these_defs thy diff_sort)