1.1 --- a/src/FOL/simpdata.ML	Mon Oct 11 14:03:40 1993 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Tue Oct 12 13:39:35 1993 +0100
     1.3 @@ -74,7 +74,9 @@
     1.4      | _ $ (Const("False",_)) => []
     1.5      | _ => [th];
     1.6  
     1.7 -fun mk_rew_rules th = map mk_meta_eq (atomize th);
     1.8 +fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
     1.9 +
    1.10 +fun mk_rew_rules th = map mk_meta_eq (atomize(gen_all th));
    1.11  
    1.12  structure Induction = InductionFun(struct val spec=IFOL.spec end);
    1.13