src/HOL/Fun.thy

   by (simp add: id_def fun_eq_iff)
 
 lemma vimage_id [simp]: "vimage id = id"
   by (simp add: id_def fun_eq_iff)
 
+code_printing
+  constant id \<rightharpoonup> (Haskell) "id"
+
 
 subsection {* The Composition Operator @{text "f \<circ> g"} *}
 
 definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
   "f o g = (\<lambda>x. f (g x))"

 
 lemma SUP_comp:
   "SUPR A (g \<circ> f) = SUPR (f ` A) g"
   by (simp add: SUP_def image_comp)
 
+code_printing
+  constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
+
 
 subsection {* The Forward Composition Operator @{text fcomp} *}
 
 definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60) where
   "f \<circ>> g = (\<lambda>x. g (f x))"

   by (simp add: fcomp_def)
 
 lemma fcomp_id [simp]: "f \<circ>> id = f"
   by (simp add: fcomp_def)
 
-code_const fcomp
-  (Eval infixl 1 "#>")
+code_printing
+  constant fcomp \<rightharpoonup> (Eval) infixl 1 "#>"
 
 no_notation fcomp (infixl "\<circ>>" 60)
 
 
 subsection {* Mapping functions *}

     end
 in proc end
 *}
 
 
-subsubsection {* Code generator *}
-
-code_const "op \<circ>"
-  (SML infixl 5 "o")
-  (Haskell infixr 9 ".")
-
-code_const "id"
-  (Haskell "id")
-
-
 subsubsection {* Functorial structure of types *}
 
 ML_file "Tools/enriched_type.ML"
 
 enriched_type map_fun: map_fun