--- a/Nominal/Ex/TypeSchemes1.thy	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/Ex/TypeSchemes1.thy	Thu Apr 19 13:57:17 2018 +0100
@@ -117,7 +117,7 @@
 nominal_function
   substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
 where
-  "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
+  "fset (atom |`| Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
   apply(simp add: eqvt_def substs_graph_aux_def)
   apply auto[2]
   apply (rule_tac y="b" and c="a" in tys.strong_exhaust)
@@ -284,7 +284,7 @@
 apply(rule_tac y="b" and c="a" in tys.strong_exhaust)
 apply(simp)
 apply(clarify)
-apply(simp only: tys.eq_iff map_fset_image)
+apply(simp only: tys.eq_iff fimage.rep_eq)
 apply(erule_tac c="Ta" in Abs_res_fcb2)
 apply(simp)
 apply(simp)