# HG changeset patch
# User blanchet
# Date 1446497389 -3600
# Node ID 0b39a1f2660489f507fd9cd1e45481d6358dd94b
# Parent  16e2313e855cf6786941d9a0d19ea25dbd15ff6f
allow selectors and discriminators with same name as type

diff -r 16e2313e855c -r 0b39a1f26604 NEWS
--- a/NEWS	Mon Nov 02 21:49:49 2015 +0100
+++ b/NEWS	Mon Nov 02 21:49:49 2015 +0100
@@ -400,6 +400,7 @@
   - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
     structure on the raw type to an abstract type defined using typedef.
   - Always generate "case_transfer" theorem.
+  - Allow discriminators and selectors with the same name as the type.
 
 * Transfer:
   - new methods for interactive debugging of 'transfer' and
diff -r 16e2313e855c -r 0b39a1f26604 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Nov 02 21:49:49 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Nov 02 21:49:49 2015 +0100
@@ -462,16 +462,22 @@
           else
             sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms raw_sel_bindingss;
 
+    val add_bindings =
+      Variable.add_fixes (distinct (op =) (filter Symbol_Pos.is_identifier
+        (map Binding.name_of (disc_bindings @ flat sel_bindingss))))
+      #> snd;
+
     val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
-    val ((((((((exh_y, xss), yss), fs), gs), u), w), (p, p'))) =
+    val ((((((((u, exh_y), xss), yss), fs), gs), w), (p, p'))) =
       no_defs_lthy
-      |> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *)
+      |> add_bindings
+      |> yield_singleton (mk_Frees fc_b_name) fcT
+      ||>> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *)
       ||>> mk_Freess "x" ctr_Tss
       ||>> mk_Freess "y" ctr_Tss
       ||>> mk_Frees "f" case_Ts
       ||>> mk_Frees "g" case_Ts
-      ||>> yield_singleton (mk_Frees fc_b_name) fcT
       ||>> yield_singleton (mk_Frees "z") B
       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT
       |> fst;
@@ -673,13 +679,14 @@
 
     fun after_qed ([exhaust_thm] :: thmss) lthy =
       let
-        val ((((((((xss, xss'), fs), gs), h), (u, u')), v), p), _) =
+        val ((((((((u, u'), (xss, xss')), fs), gs), h), v), p), _) =
           lthy
-          |> mk_Freess' "x" ctr_Tss
+          |> add_bindings
+          |> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT
+          ||>> mk_Freess' "x" ctr_Tss
           ||>> mk_Frees "f" case_Ts
           ||>> mk_Frees "g" case_Ts
           ||>> yield_singleton (mk_Frees "h") (B --> C)
-          ||>> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT
           ||>> yield_singleton (mk_Frees (fc_b_name ^ "'")) fcT
           ||>> yield_singleton (mk_Frees "P") HOLogic.boolT;
 
@@ -687,18 +694,18 @@
         val xgs = map2 (curry Term.list_comb) gs xss;
 
         val fcase = Term.list_comb (casex, fs);
-    
+
         val ufcase = fcase $ u;
         val vfcase = fcase $ v;
-    
+
         val eta_fcase = Term.list_comb (casex, eta_fs);
         val eta_gcase = Term.list_comb (casex, eta_gs);
-    
+
         val eta_ufcase = eta_fcase $ u;
         val eta_vgcase = eta_gcase $ v;
 
         fun mk_uu_eq () = HOLogic.mk_eq (u, u);
-    
+
         val uv_eq = mk_Trueprop_eq (u, v);
 
         val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;