diff -r 0a43cf458998 -r bca8203b0e91 IMP/Equiv.ML
--- a/IMP/Equiv.ML	Tue Sep 06 13:24:29 1994 +0200
+++ b/IMP/Equiv.ML	Tue Sep 06 16:15:59 1994 +0200
@@ -7,7 +7,7 @@
 goal Equiv.thy "(<a,s> -a-> n) = (A(a,s) = n)";
 by (res_inst_tac [("x","n")] spec 1);                     (* quantify n *)
 by (aexp.induct_tac "a" 1);                		  (* struct. ind. *)
-by (rewrite_goals_tac A_rewrite_rules);			  (* rewr. Den.   *)
+by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps)));	  (* rewr. Den.   *)
 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
                              addSEs aexp_elim_cases)));
 val aexp_iff = result();
@@ -19,7 +19,8 @@
 goal Equiv.thy "(<b,s> -b-> w) = (B(b,s) = w)";
 by (res_inst_tac [("x","w")] spec 1);			(* quantify w *)
 by (bexp.induct_tac "b" 1);		                (* struct. ind. *)
-by (rewrite_goals_tac B_rewrite_rules);			(* rewr. Den.   *)
+by(rewrite_goals_tac B_simps);
+  (* simplification with HOL_ss too agressive: (True=x) == True *)
 by (safe_tac (HOL_cs addSIs (aexp2::evalb.intrs)
                      addSDs [aexp1] addSEs bexp_elim_cases)
     THEN ALLGOALS(best_tac HOL_cs));
@@ -38,8 +39,8 @@
 
 (* start with rule induction *)
 be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
-
-by (rewrite_tac (Gamma_def::C_rewrite_rules));
+by (rewrite_tac (Gamma_def::C_simps));
+  (* simplification with HOL_ss again too agressive *)
 (* skip *)
 by (fast_tac comp_cs 1);
 (* assign *)
@@ -62,7 +63,7 @@
 
 goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)";
 by (com.induct_tac "c" 1);
-by (rewrite_tac C_rewrite_rules);
+by (rewrite_tac C_simps);
 by (safe_tac com_cs);
 by (ALLGOALS (asm_full_simp_tac prod_ss));