diff -r b33b42211bbf -r 188826f1ccdb Nominal/nominal_thmdecls.ML
--- a/Nominal/nominal_thmdecls.ML	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_thmdecls.ML	Mon Mar 24 15:31:17 2014 +0000
@@ -112,7 +112,7 @@
          Syntax.string_of_term (Context.proof_of context) (prop_of thm))
   in
     case prop_of thm of
-      Const ("==", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
+      Const ("Pure.eq", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
         if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then
           c
         else
@@ -256,7 +256,7 @@
 fun eqvt_transform ctxt thm =
   (case prop_of thm of @{const "Trueprop"} $ _ =>
     thm_4_of_1 ctxt thm
-  | @{const "==>"} $ _ $ _ =>
+  | @{const "Pure.imp"} $ _ $ _ =>
     thm_4_of_1 ctxt (thm_1_of_2 ctxt thm)
   | _ =>
     error msg)
@@ -279,7 +279,7 @@
     in
       (th', thm_4_of_1 ctxt thm)
     end
-  | @{const "==>"} $ _ $ _ =>
+  | @{const "Pure.imp"} $ _ $ _ =>
     let
       val th1 = thm_1_of_2 ctxt thm
     in