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: "\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