diff -r 7bc38b93a1fc -r 9ae285ce814e Nominal/nominal_thmdecls.ML
--- a/Nominal/nominal_thmdecls.ML	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/nominal_thmdecls.ML	Fri May 16 08:38:23 2014 +0100
@@ -112,7 +112,7 @@
          Syntax.string_of_term (Context.proof_of context) (prop_of thm))
   in
     case prop_of thm of
-      Const ("Pure.eq", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
+      Const (@{const_name 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 "Pure.imp"} $ _ $ _ =>
+  | @{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 "Pure.imp"} $ _ $ _ =>
+  | @{const Pure.imp} $ _ $ _ =>
     let
       val th1 = thm_1_of_2 ctxt thm
     in