--- a/src/HOL/Nominal/nominal_thmdecls.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Mar 21 20:33:56 2014 +0100
@@ -134,7 +134,7 @@
val thy = Context.theory_of context
val thms_to_be_added = (case (prop_of orig_thm) of
(* case: eqvt-lemma is of the implicational form *)
- (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
+ (Const(@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
let
val (pi,typi) = get_pi concl thy
in