diff -r 02c88bdabe75 -r 4e33894aec6d src/FOL/hypsubstdata.ML
--- a/src/FOL/hypsubstdata.ML	Sat May 14 00:32:16 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-
-(** Applying HypsubstFun to generate hyp_subst_tac **)
-structure Hypsubst_Data =
-struct
-  structure Simplifier = Simplifier
-  val dest_eq = FOLogic.dest_eq
-  val dest_Trueprop = FOLogic.dest_Trueprop
-  val dest_imp = FOLogic.dest_imp
-  val eq_reflection = @{thm eq_reflection}
-  val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
-  val imp_intr = @{thm impI}
-  val rev_mp = @{thm rev_mp}
-  val subst = @{thm subst}
-  val sym = @{thm sym}
-  val thin_refl = @{thm thin_refl}
-end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
-open Hypsubst;