diff -r 0b071f72f330 -r 16775cad1a5c src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Tue Sep 15 17:09:13 2015 +0200
@@ -66,15 +66,14 @@
 definition less_st where "F < (G::'a st) = (F \<le> G \<and> \<not> G \<le> F)"
 
 instance
-proof
-  case goal1 show ?case by(rule less_st_def)
-next
-  case goal2 show ?case by transfer (auto simp: less_eq_st_rep_def)
+proof (standard, goal_cases)
+  case 1 show ?case by(rule less_st_def)
 next
-  case goal3 thus ?case
-    by transfer (metis less_eq_st_rep_iff order_trans)
+  case 2 show ?case by transfer (auto simp: less_eq_st_rep_def)
 next
-  case goal4 thus ?case
+  case 3 thus ?case by transfer (metis less_eq_st_rep_iff order_trans)
+next
+  case 4 thus ?case
     by transfer (metis less_eq_st_rep_iff eq_st_def fun_eq_iff antisym)
 qed
 
@@ -105,15 +104,14 @@
 lift_definition top_st :: "'a st" is "[]" .
 
 instance
-proof
-  case goal1 show ?case by transfer (simp add:less_eq_st_rep_iff)
-next
-  case goal2 show ?case by transfer (simp add:less_eq_st_rep_iff)
+proof (standard, goal_cases)
+  case 1 show ?case by transfer (simp add:less_eq_st_rep_iff)
 next
-  case goal3 thus ?case by transfer (simp add:less_eq_st_rep_iff)
+  case 2 show ?case by transfer (simp add:less_eq_st_rep_iff)
 next
-  case goal4 show ?case
-    by transfer (simp add:less_eq_st_rep_iff fun_rep_map_of)
+  case 3 thus ?case by transfer (simp add:less_eq_st_rep_iff)
+next
+  case 4 show ?case by transfer (simp add:less_eq_st_rep_iff fun_rep_map_of)
 qed
 
 end