--- a/src/HOL/Hoare/HoareAbort.thy Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy Sat Jan 16 17:15:27 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/HoareAbort.thy
- ID: $Id$
Author: Leonor Prensa Nieto & Tobias Nipkow
Copyright 2003 TUM
@@ -261,7 +260,7 @@
array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70,65] 61)
translations
"P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
- "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := list_update a i v)"
+ "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
(* reverse translation not possible because of duplicate "a" *)
text{* Note: there is no special syntax for guarded array access. Thus