--- a/src/HOL/Nominal/nominal_thmdecls.ML Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Sat Aug 28 16:14:32 2010 +0200
@@ -147,7 +147,7 @@
else raise EQVT_FORM "Type Implication"
end
(* case: eqvt-lemma is of the equational form *)
- | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
+ | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $
(Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
(if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]