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