# HG changeset patch
# User haftmann
# Date 1219829072 -7200
# Node ID fe36718702aa78ee88c3042b173d9b9f24562a6c
# Parent  e892cedcd6389aa940bb22c398a5774660310de2
completing arities after subclass instance

diff -r e892cedcd638 -r fe36718702aa src/Pure/axclass.ML
--- 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 =