1.1 --- a/src/HOL/Library/Parallel.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/Library/Parallel.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -18,14 +18,10 @@
     1.4    shows "f = g"
     1.5    using assms by (cases f, cases g) (simp add: ext)
     1.6  
     1.7 -code_type future
     1.8 -  (Eval "_ future")
     1.9 -
    1.10 -code_const fork
    1.11 -  (Eval "Future.fork")
    1.12 -
    1.13 -code_const join
    1.14 -  (Eval "Future.join")
    1.15 +code_printing
    1.16 +  type_constructor future \<rightharpoonup> (Eval) "_ future"
    1.17 +| constant fork \<rightharpoonup> (Eval) "Future.fork"
    1.18 +| constant join \<rightharpoonup> (Eval) "Future.join"
    1.19  
    1.20  code_reserved Eval Future future
    1.21  
    1.22 @@ -49,14 +45,10 @@
    1.23    "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
    1.24    by (simp add: exists_def list_ex_iff)
    1.25  
    1.26 -code_const map
    1.27 -  (Eval "Par'_List.map")
    1.28 -
    1.29 -code_const forall
    1.30 -  (Eval "Par'_List.forall")
    1.31 -
    1.32 -code_const exists
    1.33 -  (Eval "Par'_List.exists")
    1.34 +code_printing
    1.35 +  constant map \<rightharpoonup> (Eval) "Par'_List.map"
    1.36 +| constant forall \<rightharpoonup> (Eval) "Par'_List.forall"
    1.37 +| constant exists \<rightharpoonup> (Eval) "Par'_List.exists"
    1.38  
    1.39  code_reserved Eval Par_List
    1.40