src/HOL/Hoare_Parallel/OG_Syntax.thy
changeset 34940 3e80eab831a1
parent 32621 a073cb249a06
child 35107 bdca9f765ee4
--- 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