
diff -r 8020249565fb -r 5976fe402824 src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -62,7 +62,7 @@
   by (simp add: supp_def Collect_disj_eq del: disj_not1)
 
 instance pat :: pt_name
-proof (default, goals)
+proof (default, goal_cases)
   case (1 x)
   show ?case by (induct x) simp_all
 next
@@ -74,7 +74,7 @@
 qed
 
 instance pat :: fs_name
-proof (default, goals)
+proof (default, goal_cases)
   case (1 x)
   show ?case by (induct x) (simp_all add: fin_supp)
 qed




