diff -r 678299eac351 -r c5cf9243ad62 src/FOL/hypsubstdata.ML
--- a/src/FOL/hypsubstdata.ML	Sun Nov 26 23:09:25 2006 +0100
+++ b/src/FOL/hypsubstdata.ML	Sun Nov 26 23:43:53 2006 +0100
@@ -6,13 +6,13 @@
   val dest_eq = FOLogic.dest_eq
   val dest_Trueprop = FOLogic.dest_Trueprop
   val dest_imp = FOLogic.dest_imp
-  val eq_reflection = eq_reflection
-  val rev_eq_reflection = meta_eq_to_obj_eq
-  val imp_intr = impI
-  val rev_mp = rev_mp
-  val subst = subst
-  val sym = sym
-  val thin_refl = prove_goal (the_context ()) "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
+  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);