diff -r fa11e1e28bd3 -r eb7c50688405 src/FOLP/simpdata.ML
--- a/src/FOLP/simpdata.ML	Thu Apr 06 11:12:35 1995 +0200
+++ b/src/FOLP/simpdata.ML	Thu Apr 06 11:14:51 1995 +0200
@@ -102,7 +102,6 @@
   end;
 
 structure FOLP_Simp = SimpFun(FOLP_SimpData);
-structure Induction = InductionFun(struct val spec=IFOLP.spec end);
 
 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
 val FOLP_congs = 
@@ -113,7 +112,7 @@
    [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
     imp_rews @ iff_rews @ quant_rews;
 
-open FOLP_Simp Induction;
+open FOLP_Simp;
 
 val auto_ss = empty_ss setauto ares_tac [TrueI];