# HG changeset patch
# User lcp
# Date 797159691 -7200
# Node ID eb7c5068840555f18c3bf4fa6a0724a82c01e3b5
# Parent  fa11e1e28bd341c5d05ddff959a40eb3bb60358f
No longer builds the induction structure (from ../Provers/ind.ML)

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];