diff -r e776a4b813d1 -r ee270328a781 src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:19 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:20 2014 +0100
@@ -128,6 +128,12 @@
 
 end
 
+definition id_rep :: "'a \<Rightarrow> 'a" where "id_rep = (\<lambda>x. x)"
+definition id_abs :: "'a \<Rightarrow> 'a" where "id_abs = (\<lambda>x. x)"
+
+lemma type_definition_id_rep_abs_UNIV: "type_definition id_rep id_abs UNIV"
+  unfolding id_rep_def id_abs_def by unfold_locales auto
+
 lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
 by (metis csum_absorb2' ordIso_transitive ordLeq_refl)
 
@@ -137,4 +143,7 @@
 ML_file "Tools/BNF/bnf_comp_tactics.ML"
 ML_file "Tools/BNF/bnf_comp.ML"
 
+hide_const id_rep id_abs
+hide_fact id_rep_def id_abs_def type_definition_id_rep_abs_UNIV
+
 end