author | nipkow |
Tue, 12 Oct 1993 13:39:35 +0100 | |
changeset 53 | f8f37a9a31dc |
parent 52 | d1b8c98e4f81 |
child 54 | 3dea30013b58 |
--- a/src/FOL/simpdata.ML Mon Oct 11 14:03:40 1993 +0100 +++ b/src/FOL/simpdata.ML Tue Oct 12 13:39:35 1993 +0100 @@ -74,7 +74,9 @@ | _ $ (Const("False",_)) => [] | _ => [th]; -fun mk_rew_rules th = map mk_meta_eq (atomize th); +fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; + +fun mk_rew_rules th = map mk_meta_eq (atomize(gen_all th)); structure Induction = InductionFun(struct val spec=IFOL.spec end);