# HG changeset patch
# User nipkow
# Date 750429575 -3600
# Node ID f8f37a9a31dcbd18bcd5d3680254ab07a7bb312e
# Parent  d1b8c98e4f81cea8bda1f0c4cb377724201c0914
Added gen_all to simpdata.ML.

diff -r d1b8c98e4f81 -r f8f37a9a31dc src/FOL/simpdata.ML
--- 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);