# HG changeset patch
# User blanchet
# Date 1393847300 -3600
# Node ID 98ad5680173a3a7d5ca3aa0979a66e6ed34b3c1b
# Parent  ee270328a78193f60702487a4bc198823a61121e
use same identity function for abs and rep (doesn't seem to confuse any proofs)

diff -r ee270328a781 -r 98ad5680173a src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:20 2014 +0100
@@ -128,11 +128,10 @@
 
 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)"
+definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp = (\<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 type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
+  unfolding id_bnf_comp_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)
@@ -143,7 +142,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
+hide_const id_bnf_comp
+hide_fact id_bnf_comp_def type_definition_id_bnf_comp_UNIV
 
 end
diff -r ee270328a781 -r 98ad5680173a src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -639,10 +639,8 @@
         else raise Term.TYPE ("mk_repT", [absT, repT, absT], [])
     | _ => raise Term.TYPE ("mk_repT", [absT, repT, absT], []));
 
-fun mk_abs_or_rep _ absU (Const (@{const_name id_abs}, _)) =
-    Const (@{const_name id_abs}, absU --> absU)
-  | mk_abs_or_rep _ absU (Const (@{const_name id_rep}, _)) =
-    Const (@{const_name id_rep}, absU --> absU)
+fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf_comp}, _)) =
+    Const (@{const_name id_bnf_comp}, absU --> absU)
   | mk_abs_or_rep getT (Type (_, Us)) abs =
     let val Ts = snd (dest_Type (getT (fastype_of abs)))
     in Term.subst_atomic_types (Ts ~~ Us) abs end;
@@ -659,9 +657,10 @@
   in
     if inline then
       pair (repT,
-        (@{const_name id_rep}, @{const_name id_abs}, @{thm type_definition_id_rep_abs_UNIV},
-         @{thm type_definition.Abs_inverse[OF type_definition_id_rep_abs_UNIV]},
-         @{thm type_definition.Abs_inject[OF type_definition_id_rep_abs_UNIV]}))
+        (@{const_name id_bnf_comp}, @{const_name id_bnf_comp},
+         @{thm type_definition_id_bnf_comp_UNIV},
+         @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_comp_UNIV]},
+         @{thm type_definition.Abs_inject[OF type_definition_id_bnf_comp_UNIV]}))
     else
       typedef (b, As, mx) set opt_morphs tac
       #>> (fn (T_name, ({Rep_name, Abs_name, ...},