# HG changeset patch
# User wenzelm
# Date 882191646 -3600
# Node ID 2af86fcb97d71eaafef2d234ad719df0d84c5394
# Parent  ad74412ef7a0d15ee2e3607113002894fcc3d432
No longer depend on theory context!

diff -r ad74412ef7a0 -r 2af86fcb97d7 src/HOL/typedef.ML
--- 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