src/Pure/axclass.ML
changeset 3632 17527284f100
parent 3395 d8700b008944
child 3764 fe7719aee219
     1.1 --- a/src/Pure/axclass.ML	Wed Aug 06 14:42:44 1997 +0200
     1.2 +++ b/src/Pure/axclass.ML	Wed Aug 06 15:07:33 1997 +0200
     1.3 @@ -285,15 +285,17 @@
     1.4  
     1.5  (** add proved subclass relations and arities **)
     1.6  
     1.7 -fun add_inst_subclass (c1, c2) axms thms usr_tac thy =
     1.8 +fun add_inst_subclass c1_c2 axms thms usr_tac thy =
     1.9 + (writeln ("Proving class inclusion " ^ quote (Sorts.str_of_classrel c1_c2) ^ " ...");
    1.10    add_classrel_thms
    1.11 -  [prove_subclass thy (c1, c2) (witnesses thy axms thms) usr_tac] thy;
    1.12 +    [prove_subclass thy c1_c2 (witnesses thy axms thms) usr_tac] thy);
    1.13  
    1.14  fun add_inst_arity (t, ss, cs) axms thms usr_tac thy =
    1.15    let
    1.16      val wthms = witnesses thy axms thms;
    1.17      fun prove c =
    1.18 -      prove_arity thy (t, ss, c) wthms usr_tac;
    1.19 +     (writeln ("Proving type arity " ^ quote (Sorts.str_of_arity (t, ss, [c])) ^ " ...");
    1.20 +      prove_arity thy (t, ss, c) wthms usr_tac);
    1.21    in
    1.22      add_arity_thms (map prove cs) thy
    1.23    end;