diff -r b72e0a9d62b9 -r 83b3c110f22d src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Mar 22 18:15:09 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Mar 22 18:16:54 2014 +0100
@@ -87,8 +87,8 @@
   | get_inner_fresh_fun (v as Var _)  = NONE
   | get_inner_fresh_fun (Const _) = NONE
   | get_inner_fresh_fun (Abs (_, _, t)) = get_inner_fresh_fun t
-  | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u)
-                           = SOME T
+  | get_inner_fresh_fun (Const (@{const_name Nominal.fresh_fun},
+      Type(@{type_name fun},[Type (@{type_name fun},[Type (T,_),_]),_])) $ u) = SOME T
   | get_inner_fresh_fun (t $ u) =
      let val a = get_inner_fresh_fun u in
      if a = NONE then get_inner_fresh_fun t else a