--- a/src/HOL/Nominal/nominal_fresh_fun.ML Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sat Jan 05 17:24:33 2019 +0100
@@ -90,8 +90,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 (@{const_name Nominal.fresh_fun},
- Type(@{type_name fun},[Type (@{type_name fun},[Type (T,_),_]),_])) $ u) = SOME T
+ | get_inner_fresh_fun (Const (\<^const_name>\<open>Nominal.fresh_fun\<close>,
+ Type(\<^type_name>\<open>fun\<close>,[Type (\<^type_name>\<open>fun\<close>,[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