--- a/Nominal/Nominal2_Abs.thy	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Nominal2_Abs.thy	Sat Mar 19 21:06:48 2016 +0000
@@ -537,7 +537,7 @@
   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
 instance
-  apply(default)
+  apply standard
   apply(case_tac [!] x)
   apply(simp_all)
   done
@@ -559,7 +559,7 @@
   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
 instance
-  apply(default)
+  apply standard
   apply(case_tac [!] x)
   apply(simp_all)
   done
@@ -581,7 +581,7 @@
   by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
 
 instance
-  apply(default)
+  apply standard
   apply(case_tac [!] x)
   apply(simp_all)
   done
@@ -700,19 +700,19 @@
 by (simp_all add: Abs_finite_supp finite_supp)
 
 instance abs_set :: (fs) fs
-  apply(default)
+  apply standard
   apply(case_tac x)
   apply(simp add: supp_Abs finite_supp)
   done
 
 instance abs_res :: (fs) fs
-  apply(default)
+  apply standard
   apply(case_tac x)
   apply(simp add: supp_Abs finite_supp)
   done
 
 instance abs_lst :: (fs) fs
-  apply(default)
+  apply standard
   apply(case_tac x)
   apply(simp add: supp_Abs finite_supp)
   done
@@ -933,7 +933,7 @@
       |> Thm.cterm_of ctxt
     val cvrs_ty = Thm.ctyp_of_cterm cvrs
     val thm' = thm
-      |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] 
+      |> Thm.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] 
   in
     SOME thm'
   end