author | paulson |
Mon, 14 Jul 1997 12:44:09 +0200 | |
changeset 3518 | 6e11c7bfb9c7 |
parent 3517 | 2547f33fa33a |
child 3519 | ab0a9fbed4c0 |
--- a/src/HOL/simpdata.ML Mon Jul 14 12:42:28 1997 +0200 +++ b/src/HOL/simpdata.ML Mon Jul 14 12:44:09 1997 +0200 @@ -41,7 +41,7 @@ | (con $ _ $ _) => if con=iff_const then Delrules [zero_var_indexes (th RS iffD2), - zero_var_indexes (th RS iffD1)] + make_elim (zero_var_indexes (th RS iffD1))] else Delrules [th] | _ => Delrules [th]; Delsimps [th])