--- 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