diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/TypeSchemes2.thy
--- a/Nominal/Ex/TypeSchemes2.thy	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/Ex/TypeSchemes2.thy	Thu Apr 19 13:57:17 2018 +0100
@@ -2,6 +2,7 @@
 imports "../Nominal2"
 begin
 
+  
 section {*** Type Schemes defined as a single nominal datatype ***}
 
 atom_decl name 
@@ -60,14 +61,14 @@
   shows "(p \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl (p \<bullet> (f x))"
 using a
 by clarsimp
-
+  
 nominal_function (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
 where
   "subst \<theta> (Var X) = lookup \<theta> X"
 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
-| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
+| "fset (atom |`| xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
 thm subst_substs_graph_def subst_substs_graph_aux_def
 apply(simp add: subst_substs_graph_aux_def eqvt_def)
 apply(rule TrueI)