--- a/src/HOL/IMP/Abs_Int3.thy Sun Jan 20 15:34:27 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy Fri Jan 25 16:45:09 2013 +0100
@@ -416,14 +416,14 @@
value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
-value "show_acom_opt (AI_ivl' test3_ivl)"
+value "show_acom (the(AI_ivl' test3_ivl))"
text{* Now all the analyses terminate: *}
-value "show_acom_opt (AI_ivl' test4_ivl)"
-value "show_acom_opt (AI_ivl' test5_ivl)"
-value "show_acom_opt (AI_ivl' test6_ivl)"
+value "show_acom (the(AI_ivl' test4_ivl))"
+value "show_acom (the(AI_ivl' test5_ivl))"
+value "show_acom (the(AI_ivl' test6_ivl))"
subsubsection "Generic Termination Proof"