diff -r 13bd3d12ec2f -r 444bb25d3da0 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Mon Nov 29 18:49:35 2004 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Tue Nov 30 06:50:03 2004 +0100
@@ -131,7 +131,7 @@
  apply assumption
 apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) 
   --{*essential for speed*}
-txt{*Blast_tac with new substOccur fails*}
+txt{*Blast with new substOccur fails*}
 apply (fast intro: converse_rtrancl_into_rtrancl)
 done