No longer depend on theory context!

--- a/src/HOL/typedef.ML	Sat Dec 13 17:27:16 1997 +0100
+++ b/src/HOL/typedef.ML	Mon Dec 15 14:14:06 1997 +0100
@@ -31,7 +31,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));
+      if_none usr_tac (TRY (ALLGOALS (CLASET' blast_tac)));
   in
     prove_goalw_cterm [] goal (K [tac])
   end