--- a/src/HOL/Record.thy Tue Dec 18 22:21:42 2007 +0100
+++ b/src/HOL/Record.thy Wed Dec 19 16:32:12 2007 +0100
@@ -19,15 +19,8 @@
lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
by simp
-constdefs
- K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
- 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)
-
-lemma K_record_cong [cong]: "K_record c x = K_record c x"
- by (rule refl)
+lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
+ by (simp add: comp_def)
subsection {* Concrete record syntax *}