src/HOL/Hoare_Parallel/OG_Syntax.thy

 translations
   "_prg c q" \<rightleftharpoons> "[(Some c, q)]"
   "_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
     fun quote_tr' f (t :: ts) =
           Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)