# HG changeset patch
# User paulson
# Date 881143224 -3600
# Node ID d565d2197a5f122b26bfcc36739240e05a6f91ef
# Parent  7ac9f3e8a97daff285767cf0e83b2ddeb0325998
updated for latest Blast_tac, which treats equality differently

diff -r 7ac9f3e8a97d -r d565d2197a5f src/HOL/ex/MT.ML
--- 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)";
diff -r 7ac9f3e8a97d -r d565d2197a5f src/HOL/ex/cla.ML
--- 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";