--- 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
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat Jan 16 17:15:27 2010 +0100
@@ -72,7 +72,7 @@
"_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps"
"_PAR ps" \<rightleftharpoons> "Parallel ps"
- "_prg_scheme j i k c q" \<rightleftharpoons> "map (\<lambda>i. (Some c, q)) [j..<k]"
+ "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (Some c, q)) [j..<k]"
print_translation {*
let
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat Jan 16 17:15:27 2010 +0100
@@ -43,7 +43,7 @@
"_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs" ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57)
translations
- "_prg_scheme j i k c" \<rightleftharpoons> "(map (\<lambda>i. c) [j..<k])"
+ "_prg_scheme j i k c" \<rightleftharpoons> "(CONST map (\<lambda>i. c) [j..<k])"
text {* Translations for variables before and after a transition: *}