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.
completing arities after subclass instance
authorhaftmann
Wed, 27 Aug 2008 11:24:32 +0200
changeset 28014 fe36718702aa
parent 28013 e892cedcd638
child 28015 11635f41abc1
completing arities after subclass instance
src/Pure/axclass.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/axclass.ML	Wed Aug 27 11:24:31 2008 +0200
+++ b/src/Pure/axclass.ML	Wed Aug 27 11:24:32 2008 +0200
@@ -296,6 +296,7 @@
     thy
     |> Sign.primitive_classrel (c1, c2)
     |> put_classrel ((c1, c2), Drule.unconstrainTs th)
+    |> perhaps complete_arities
   end;
 
 fun add_arity th thy =
isabelle