updated for latest Blast_tac, which treats equality differently

--- a/src/HOL/ex/MT.ML	Wed Dec 03 10:52:17 1997 +0100
+++ b/src/HOL/ex/MT.ML	Wed Dec 03 11:00:24 1997 +0100
@@ -418,7 +418,7 @@
 fun elab_e_elim_tac p = 
   ( (rtac elab_elim 1) THEN 
     (resolve_tac p 1) THEN 
-    (REPEAT (blast_tac (e_ext_cs HOL_cs) 1))
+    (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
   );
 
 val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";

--- a/src/HOL/ex/cla.ML	Wed Dec 03 10:52:17 1997 +0100
+++ b/src/HOL/ex/cla.ML	Wed Dec 03 11:00:24 1997 +0100
@@ -386,7 +386,7 @@
 by (assume_tac 1);
 by (res_inst_tac [("x","b")] allE 1);
 by (assume_tac 1);
-by (Blast_tac 1);
+by (Fast_tac 1);    (*Blast_tac's treatment of equality can't do it*)
 result();
 
 writeln"Problem 50";