diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/Example.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -1247,7 +1247,7 @@
 abbreviation "s9' == (Some (Xcpt (Std IndOutBound)), s8)"
 
 
-declare Pair_eq [simp del]
+declare prod.inject [simp del]
 schematic_goal exec_test: 
 "\<lbrakk>the (new_Addr (heap  s1)) = a;  
   the (new_Addr (heap ?s2)) = b;  
@@ -1377,6 +1377,6 @@
 apply  (simp (no_asm_simp))
 apply (auto simp add: in_bounds_def)
 done
-declare Pair_eq [simp]
+declare prod.inject [simp]
 
 end