# HG changeset patch
# User haftmann
# Date 1263658527 -3600
# Node ID 3e80eab831a1d93490979c84958c21a9a65cb144
# Parent  44294cfecb1d1ac107ad434d4cf854ba4df99cac
explicit CONST in translations

diff -r 44294cfecb1d -r 3e80eab831a1 src/HOL/Hoare/HoareAbort.thy
--- 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
diff -r 44294cfecb1d -r 3e80eab831a1 src/HOL/Hoare_Parallel/OG_Syntax.thy
--- 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
diff -r 44294cfecb1d -r 3e80eab831a1 src/HOL/Hoare_Parallel/RG_Syntax.thy
--- 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: *}