# HG changeset patch
# User haftmann
# Date 1196449985 -3600
# Node ID 54db9b5080b8dacccb14d0cf2e9746ee2e9c8bdd
# Parent  38c15efe603bb98e6a84e08295f7100fc831b4ae
more canonical attribute application

diff -r 38c15efe603b -r 54db9b5080b8 src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Fri Nov 30 20:13:03 2007 +0100
+++ b/src/HOL/Bali/State.thy	Fri Nov 30 20:13:05 2007 +0100
@@ -290,7 +290,7 @@
   init_vals     :: "('a, ty) table \<Rightarrow> ('a, val) table"
 
 translations
- "init_vals vs"    == "option_map default_val \<circ> vs"
+ "init_vals vs"    == "CONST option_map default_val \<circ> vs"
 
 lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
 apply (unfold arr_comps_def in_bounds_def)
diff -r 38c15efe603b -r 54db9b5080b8 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Fri Nov 30 20:13:03 2007 +0100
+++ b/src/HOL/Datatype.thy	Fri Nov 30 20:13:05 2007 +0100
@@ -652,11 +652,10 @@
 lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
   by (cases xo) auto
 
-constdefs
-  option_map :: "('a => 'b) => ('a option => 'b option)"
-  "option_map == %f y. case y of None => None | Some x => Some (f x)"
-
-lemmas [code func del] = option_map_def
+definition
+  option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
+where
+  [code func del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
 
 lemma option_map_None [simp, code]: "option_map f None = None"
   by (simp add: option_map_def)
diff -r 38c15efe603b -r 54db9b5080b8 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Nov 30 20:13:03 2007 +0100
+++ b/src/HOL/Product_Type.thy	Fri Nov 30 20:13:05 2007 +0100
@@ -771,12 +771,11 @@
   Setup of internal @{text split_rule}.
 *}
 
-constdefs
-  internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
+definition
+  internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
+where
   "internal_split == split"
 
-lemmas [code func del] = internal_split_def
-
 lemma internal_split_conv: "internal_split c (a, b) = c a b"
   by (simp only: internal_split_def split_conv)