# HG changeset patch
# User wenzelm
# Date 965422591 -7200
# Node ID 95852b4be2147e69ba409f1018340ab4d6f719c5
# Parent  de95b5125580b27d44067b405f3a3d2b0b2a890c
rev_eq_reflection = meta_eq_to_obj_eq;

diff -r de95b5125580 -r 95852b4be214 src/FOL/hypsubstdata.ML
--- a/src/FOL/hypsubstdata.ML	Fri Aug 04 22:56:11 2000 +0200
+++ b/src/FOL/hypsubstdata.ML	Fri Aug 04 22:56:31 2000 +0200
@@ -8,6 +8,7 @@
   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