src/HOL/Option.ML

--- a/src/HOL/Option.ML	Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Option.ML	Fri Apr 11 15:21:36 1997 +0200
@@ -11,7 +11,7 @@
 val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
  br (prem RS rev_mp) 1;
  by (option.induct_tac "opt" 1);
- by (ALLGOALS(Fast_tac));
+ by (ALLGOALS Blast_tac);
 bind_thm("optionE", standard(result() RS disjE));
 (*
 goal Option.thy "opt=None | (? x.opt=Some(x))";