--- a/Nominal/Ex/Lambda.thy	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/Ex/Lambda.thy	Thu Apr 19 13:57:17 2018 +0100
@@ -152,7 +152,7 @@
 section {* Paths to a free variables *} 
 
 instance path :: pure
-apply(default)
+apply(standard)
 apply(induct_tac "x::path" rule: path.induct)
 apply(simp_all)
 done
@@ -615,7 +615,7 @@
 | DBLam db
 
 instance db :: pure
-  apply default
+  apply standard
   apply (induct_tac x rule: db.induct)
   apply (simp_all add: permute_pure)
   done
@@ -930,7 +930,7 @@
   and x y::"'a::at"
   shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa
      \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"
-  by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair)
+  by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff fresh_Pair)
 
 nominal_function
   aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool"