src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Fri Apr 27 14:21:23 2007 +0200
+++ b/src/FOL/simpdata.ML	Fri Apr 27 16:31:20 2007 +0200
@@ -275,11 +275,6 @@
 
 (*** Standard simpsets ***)
 
-structure Induction = InductionFun(struct val spec = spec end);
-
-open Induction;
-
-
 bind_thms ("meta_simps",
  [triv_forall_equality,   (* prunes params *)
   thm "True_implies_equals"]);  (* prune asms `True' *)