--- a/src/Provers/hypsubst.ML Mon Aug 08 16:38:59 2011 +0200
+++ b/src/Provers/hypsubst.ML Mon Aug 08 17:23:15 2011 +0200
@@ -116,8 +116,7 @@
(*For the simpset. Adds ALL suitable equalities, even if not first!
No vars are allowed here, as simpsets are built from meta-assumptions*)
fun mk_eqs bnd th =
- [ if inspect_pair bnd false (Data.dest_eq
- (Data.dest_Trueprop (#prop (rep_thm th))))
+ [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th)))
then th RS Data.eq_reflection
else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
handle TERM _ => [] | Match => [];