# HG changeset patch
# User wenzelm
# Date 870872853 -7200
# Node ID 17527284f100e71f28004f3d3001ca9f330b1949
# Parent  88a279998f907cb69b19a4bf2e29d34fa3730794
added "Proving ..." msgs;

diff -r 88a279998f90 -r 17527284f100 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Aug 06 14:42:44 1997 +0200
+++ b/src/Pure/axclass.ML	Wed Aug 06 15:07:33 1997 +0200
@@ -285,15 +285,17 @@
 
 (** add proved subclass relations and arities **)
 
-fun add_inst_subclass (c1, c2) axms thms usr_tac thy =
+fun add_inst_subclass c1_c2 axms thms usr_tac thy =
+ (writeln ("Proving class inclusion " ^ quote (Sorts.str_of_classrel c1_c2) ^ " ...");
   add_classrel_thms
-  [prove_subclass thy (c1, c2) (witnesses thy axms thms) usr_tac] thy;
+    [prove_subclass thy c1_c2 (witnesses thy axms thms) usr_tac] thy);
 
 fun add_inst_arity (t, ss, cs) axms thms usr_tac thy =
   let
     val wthms = witnesses thy axms thms;
     fun prove c =
-      prove_arity thy (t, ss, c) wthms usr_tac;
+     (writeln ("Proving type arity " ^ quote (Sorts.str_of_arity (t, ss, [c])) ^ " ...");
+      prove_arity thy (t, ss, c) wthms usr_tac);
   in
     add_arity_thms (map prove cs) thy
   end;