| changeset 1264 | 3eb91524b938 |
| parent 1125 | 13a3df2adbe5 |
| child 1465 | 5d7a7e439cec |
--- a/src/HOL/Lfp.ML Wed Oct 04 13:01:05 1995 +0100 +++ b/src/HOL/Lfp.ML Wed Oct 04 13:10:03 1995 +0100 @@ -59,7 +59,7 @@ brs prems 1; by(res_inst_tac[("p","x")]PairE 1); by(hyp_subst_tac 1); -by(asm_simp_tac (prod_ss addsimps prems) 1); +by(asm_simp_tac (!simpset addsimps prems) 1); qed"induct2"; (*** Fixpoint induction a la David Park ***)