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