src/HOL/Lambda/ParRed.ML
changeset 3207 fe79ad367d77
parent 2922 580647a879cf
child 4089 96fba19bcbe2
--- a/src/HOL/Lambda/ParRed.ML	Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Thu May 15 15:51:47 1997 +0200
@@ -86,7 +86,7 @@
  by (etac rev_mp 1);
  by (dB.induct_tac "dB1" 1);
  by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] 
-                                unsafe_addss (!simpset))));
+                                addss (!simpset))));
 qed_spec_mp "par_beta_cd";
 
 (*** Confluence (via cd) ***)