src/HOL/Library/Parallel.thy
changeset 81706 7beb0cf38292
parent 60500 903bb1495239
--- a/src/HOL/Library/Parallel.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/Parallel.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -23,7 +23,7 @@
 | constant fork \<rightharpoonup> (Eval) "Future.fork"
 | constant join \<rightharpoonup> (Eval) "Future.join"
 
-code_reserved Eval Future future
+code_reserved (Eval) Future future
 
 
 subsection \<open>Parallel lists\<close>
@@ -50,7 +50,7 @@
 | constant forall \<rightharpoonup> (Eval) "Par'_List.forall"
 | constant exists \<rightharpoonup> (Eval) "Par'_List.exists"
 
-code_reserved Eval Par_List
+code_reserved (Eval) Par_List
 
 
 hide_const (open) fork join map exists forall