diff -r 0b071f72f330 -r 16775cad1a5c src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Tue Sep 15 17:09:13 2015 +0200
@@ -11,14 +11,14 @@
 definition "less_prod p1 p2 = (p1 \<le> p2 \<and> \<not> p2 \<le> (p1::'a*'b))"
 
 instance
-proof
-  case goal1 show ?case by(rule less_prod_def)
+proof (standard, goal_cases)
+  case 1 show ?case by(rule less_prod_def)
 next
-  case goal2 show ?case by(simp add: less_eq_prod_def)
+  case 2 show ?case by(simp add: less_eq_prod_def)
 next
-  case goal3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
+  case 3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
 next
-  case goal4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
+  case 4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
 qed
 
 end