# HG changeset patch
# User lcp
# Date 783623249 -3600
# Node ID 1922f98b8f7ee8bc361dbe89e5d77d9e5a896c70
# Parent  e0be228a9c5bfb319dd9d89db3cef4157730b50b
com1,2: added simplifier calls to remove use of ssubst in fast_tac

diff -r e0be228a9c5b -r 1922f98b8f7e src/ZF/IMP/Equiv.ML
--- a/src/ZF/IMP/Equiv.ML	Mon Oct 31 18:03:14 1994 +0100
+++ b/src/ZF/IMP/Equiv.ML	Mon Oct 31 18:07:29 1994 +0100
@@ -59,23 +59,25 @@
 by (fast_tac comp_cs 1);
 
 (* assign *)
-by (asm_full_simp_tac (ZF_ss addsimps [aexp1,assign_type] @
-                                      op_type_intrs) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [aexp1,assign_type] @ op_type_intrs) 1);
+
 (* comp *)
 by (fast_tac comp_cs 1);
 
 (* if *)
-by (fast_tac (ZF_cs addSIs [bexp1] addIs  [(fst_conv RS ssubst)]) 1);
-by (fast_tac (ZF_cs addSIs [bexp1] addIs  [(fst_conv RS ssubst)]) 1);
+by (asm_simp_tac (ZF_ss addsimps [bexp1]) 1);
+by (asm_simp_tac (ZF_ss addsimps [bexp1]) 1);
 
 (* while *)
-by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
-by (fast_tac (comp_cs addSIs [bexp1,idI]@evalb_type_intrs
-                      addIs  [(fst_conv RS ssubst)]) 1);
+by (etac (rewrite_rule [Gamma_def]
+	  (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
+by (asm_simp_tac (ZF_ss addsimps [bexp1]) 1);
+by (fast_tac (comp_cs addSIs [bexp1,idI]@evalb_type_intrs) 1);
 
-by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
-by (fast_tac (comp_cs addSIs [bexp1,compI]@evalb_type_intrs
-                      addIs  [(fst_conv RS ssubst)]) 1);
+by (etac (rewrite_rule [Gamma_def]
+	  (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
+by (asm_simp_tac (ZF_ss addsimps [bexp1]) 1);
+by (fast_tac (comp_cs addSIs [bexp1,compI]@evalb_type_intrs) 1);
 
 val com1 = result();