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