diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -62,7 +62,7 @@
   by (simp add: supp_def Collect_disj_eq del: disj_not1)
 
 instance pat :: pt_name
-proof (default, goal_cases)
+proof (standard, goal_cases)
   case (1 x)
   show ?case by (induct x) simp_all
 next
@@ -74,7 +74,7 @@
 qed
 
 instance pat :: fs_name
-proof (default, goal_cases)
+proof (standard, goal_cases)
   case (1 x)
   show ?case by (induct x) (simp_all add: fin_supp)
 qed