--- a/src/HOL/Record.thy Fri Apr 20 17:58:24 2007 +0200
+++ b/src/HOL/Record.thy Fri Apr 20 17:58:25 2007 +0200
@@ -17,10 +17,9 @@
lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
by simp
-definition
+constdefs
K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
-where
- K_record_apply [simp]: "K_record c x = c"
+ K_record_apply [simp, code func]: "K_record c x \<equiv> c"
lemma K_record_comp [simp]: "(K_record c \<circ> f) = K_record c"
by (rule ext) (simp add: K_record_apply comp_def)