--- 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