Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
prevent potential failure
authorhaftmann
Tue, 28 Apr 2009 13:34:48 +0200
changeset 31012 751f5aa3e315
parent 31011 506e57123cd1
child 31013 69a476d6fea6
child 31014 79f0858d9d49
prevent potential failure
src/Pure/Isar/class_target.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle