1.1 --- a/src/HOL/Fun.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -29,6 +29,9 @@
     1.4  lemma vimage_id [simp]: "vimage id = id"
     1.5    by (simp add: id_def fun_eq_iff)
     1.6  
     1.7 +code_printing
     1.8 +  constant id \<rightharpoonup> (Haskell) "id"
     1.9 +
    1.10  
    1.11  subsection {* The Composition Operator @{text "f \<circ> g"} *}
    1.12  
    1.13 @@ -77,6 +80,9 @@
    1.14    "SUPR A (g \<circ> f) = SUPR (f ` A) g"
    1.15    by (simp add: SUP_def image_comp)
    1.16  
    1.17 +code_printing
    1.18 +  constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
    1.19 +
    1.20  
    1.21  subsection {* The Forward Composition Operator @{text fcomp} *}
    1.22  
    1.23 @@ -95,8 +101,8 @@
    1.24  lemma fcomp_id [simp]: "f \<circ>> id = f"
    1.25    by (simp add: fcomp_def)
    1.26  
    1.27 -code_const fcomp
    1.28 -  (Eval infixl 1 "#>")
    1.29 +code_printing
    1.30 +  constant fcomp \<rightharpoonup> (Eval) infixl 1 "#>"
    1.31  
    1.32  no_notation fcomp (infixl "\<circ>>" 60)
    1.33  
    1.34 @@ -814,16 +820,6 @@
    1.35  *}
    1.36  
    1.37  
    1.38 -subsubsection {* Code generator *}
    1.39 -
    1.40 -code_const "op \<circ>"
    1.41 -  (SML infixl 5 "o")
    1.42 -  (Haskell infixr 9 ".")
    1.43 -
    1.44 -code_const "id"
    1.45 -  (Haskell "id")
    1.46 -
    1.47 -
    1.48  subsubsection {* Functorial structure of types *}
    1.49  
    1.50  ML_file "Tools/enriched_type.ML"