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