| changeset 4091 | 771b1f6422a8 |
| parent 2469 | b50b8c0eec01 |
| child 5050 | e925308df78b |
--- a/src/FOL/ex/NatClass.ML Mon Nov 03 12:22:43 1997 +0100 +++ b/src/FOL/ex/NatClass.ML Mon Nov 03 12:24:13 1997 +0100 @@ -57,5 +57,5 @@ val [prem] = goal NatClass.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; by (res_inst_tac [("n","i")] induct 1); by (Simp_tac 1); -by (asm_simp_tac (!simpset addsimps [prem]) 1); +by (asm_simp_tac (simpset() addsimps [prem]) 1); result();