diff -r aafd4270b4d4 -r 3371f5ee4ace src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Sun Jan 20 15:34:27 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Fri Jan 25 16:45:09 2013 +0100
@@ -80,17 +80,17 @@
 value "show_acom (steps test1_const 1)"
 value "show_acom (steps test1_const 2)"
 value "show_acom (steps test1_const 3)"
-value "show_acom_opt (AI_const test1_const)"
+value "show_acom (the(AI_const test1_const))"
 
-value "show_acom_opt (AI_const test2_const)"
-value "show_acom_opt (AI_const test3_const)"
+value "show_acom (the(AI_const test2_const))"
+value "show_acom (the(AI_const test3_const))"
 
 value "show_acom (steps test4_const 0)"
 value "show_acom (steps test4_const 1)"
 value "show_acom (steps test4_const 2)"
 value "show_acom (steps test4_const 3)"
 value "show_acom (steps test4_const 4)"
-value "show_acom_opt (AI_const test4_const)"
+value "show_acom (the(AI_const test4_const))"
 
 value "show_acom (steps test5_const 0)"
 value "show_acom (steps test5_const 1)"
@@ -99,7 +99,7 @@
 value "show_acom (steps test5_const 4)"
 value "show_acom (steps test5_const 5)"
 value "show_acom (steps test5_const 6)"
-value "show_acom_opt (AI_const test5_const)"
+value "show_acom (the(AI_const test5_const))"
 
 value "show_acom (steps test6_const 0)"
 value "show_acom (steps test6_const 1)"
@@ -115,7 +115,7 @@
 value "show_acom (steps test6_const 11)"
 value "show_acom (steps test6_const 12)"
 value "show_acom (steps test6_const 13)"
-value "show_acom_opt (AI_const test6_const)"
+value "show_acom (the(AI_const test6_const))"
 
 
 text{* Monotonicity: *}