| changeset 2637 | e9b203f854ae |
| parent 2159 | e650a3f6f600 |
| child 2891 | d8f254ad1ab9 |
--- a/src/HOL/Lambda/ParRed.ML Sat Feb 15 17:48:19 1997 +0100 +++ b/src/HOL/Lambda/ParRed.ML Sat Feb 15 17:52:31 1997 +0100 @@ -83,7 +83,7 @@ by (Simp_tac 1); by (etac rev_mp 1); by (dB.induct_tac "dB1" 1); - by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] addss !simpset))); + by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] unsafe_addss (!simpset)))); qed_spec_mp "par_beta_cd"; (*** Confluence (via cd) ***)