Added trace output and replaced fast_tac set_cs by Fast_tac.

--- a/src/HOL/typedef.ML	Wed Apr 09 15:56:53 1997 +0200
+++ b/src/HOL/typedef.ML	Thu Apr 10 09:08:05 1997 +0200
@@ -33,7 +33,7 @@
     val tac =
       TRY (rewrite_goals_tac (filter is_def thms)) THEN
       TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN
-      if_none usr_tac (TRY (ALLGOALS (fast_tac set_cs)));
+      if_none usr_tac (TRY (ALLGOALS Fast_tac));
   in
     prove_goalw_cterm [] goal (K [tac])
   end
@@ -103,6 +103,7 @@
     if null errs then ()
     else error (cat_lines errs);
 
+    writeln("Proving nonemptiness of " ^ quote name ^ " ...");
     prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
 
     thy