1.1 --- a/src/HOL/Bali/State.thy	Fri Nov 30 20:13:03 2007 +0100
     1.2 +++ b/src/HOL/Bali/State.thy	Fri Nov 30 20:13:05 2007 +0100
     1.3 @@ -290,7 +290,7 @@
     1.4    init_vals     :: "('a, ty) table \<Rightarrow> ('a, val) table"
     1.5  
     1.6  translations
     1.7 - "init_vals vs"    == "option_map default_val \<circ> vs"
     1.8 + "init_vals vs"    == "CONST option_map default_val \<circ> vs"
     1.9  
    1.10  lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
    1.11  apply (unfold arr_comps_def in_bounds_def)

     2.1 --- a/src/HOL/Datatype.thy	Fri Nov 30 20:13:03 2007 +0100
     2.2 +++ b/src/HOL/Datatype.thy	Fri Nov 30 20:13:05 2007 +0100
     2.3 @@ -652,11 +652,10 @@
     2.4  lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
     2.5    by (cases xo) auto
     2.6  
     2.7 -constdefs
     2.8 -  option_map :: "('a => 'b) => ('a option => 'b option)"
     2.9 -  "option_map == %f y. case y of None => None | Some x => Some (f x)"
    2.10 -
    2.11 -lemmas [code func del] = option_map_def
    2.12 +definition
    2.13 +  option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
    2.14 +where
    2.15 +  [code func del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
    2.16  
    2.17  lemma option_map_None [simp, code]: "option_map f None = None"
    2.18    by (simp add: option_map_def)

     3.1 --- a/src/HOL/Product_Type.thy	Fri Nov 30 20:13:03 2007 +0100
     3.2 +++ b/src/HOL/Product_Type.thy	Fri Nov 30 20:13:05 2007 +0100
     3.3 @@ -771,12 +771,11 @@
     3.4    Setup of internal @{text split_rule}.
     3.5  *}
     3.6  
     3.7 -constdefs
     3.8 -  internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
     3.9 +definition
    3.10 +  internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
    3.11 +where
    3.12    "internal_split == split"
    3.13  
    3.14 -lemmas [code func del] = internal_split_def
    3.15 -
    3.16  lemma internal_split_conv: "internal_split c (a, b) = c a b"
    3.17    by (simp only: internal_split_def split_conv)
    3.18