# HG changeset patch
# User nipkow
# Date 860656085 -7200
# Node ID c0e3f1ceabf25e368e2ce0805e101b57403e93b1
# Parent  56131a902972b7759911deddc4cda84e820e8d1d
Added trace output and replaced fast_tac set_cs by Fast_tac.

diff -r 56131a902972 -r c0e3f1ceabf2 src/HOL/typedef.ML
--- 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