1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 00:20:37 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 00:55:11 2012 +0200
     1.3 @@ -127,18 +127,20 @@
     1.4        Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
     1.5          unsorted_As);
     1.6  
     1.7 -    val bs = map type_binder_of specs;
     1.8 -    val fake_Ts = map mk_fake_T bs;
     1.9 +    val fp_bs = map type_binder_of specs;
    1.10 +    val fake_Ts = map mk_fake_T fp_bs;
    1.11  
    1.12      val mixfixes = map mixfix_of specs;
    1.13  
    1.14 -    val _ = (case duplicates Binding.eq_name bs of [] => ()
    1.15 +    val _ = (case duplicates Binding.eq_name fp_bs of [] => ()
    1.16        | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b)));
    1.17  
    1.18      val ctr_specss = map ctr_specs_of specs;
    1.19  
    1.20      val disc_binderss = map (map disc_of) ctr_specss;
    1.21 -    val ctr_binderss = map (map ctr_of) ctr_specss;
    1.22 +    val ctr_binderss =
    1.23 +      map2 (fn fp_b => map (Binding.qualify false (Binding.name_of fp_b) o ctr_of))
    1.24 +        fp_bs ctr_specss;
    1.25      val ctr_argsss = map (map args_of) ctr_specss;
    1.26      val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
    1.27  
    1.28 @@ -176,7 +178,7 @@
    1.29  
    1.30      val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects,
    1.31          fp_iter_thms, fp_rec_thms), lthy)) =
    1.32 -      fp_bnf (if lfp then bnf_lfp else bnf_gfp) bs mixfixes (map dest_TFree unsorted_As) fp_eqs
    1.33 +      fp_bnf (if lfp then bnf_lfp else bnf_gfp) fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs
    1.34          no_defs_lthy0;
    1.35  
    1.36      val add_nested_bnf_names =
    1.37 @@ -329,7 +331,7 @@
    1.38              (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss))))
    1.39          end;
    1.40  
    1.41 -    fun define_ctrs_case_for_type ((((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec),
    1.42 +    fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec),
    1.43            fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_binders), ctr_mixfixes), ctr_Tss),
    1.44          disc_binders), sel_binderss), raw_sel_defaultss) no_defs_lthy =
    1.45        let
    1.46 @@ -349,7 +351,7 @@
    1.47            map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $
    1.48              mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss;
    1.49  
    1.50 -        val case_binder = Binding.suffix_name ("_" ^ caseN) b;
    1.51 +        val case_binder = Binding.suffix_name ("_" ^ caseN) fp_b;
    1.52  
    1.53          val case_rhs =
    1.54            fold_rev Term.lambda (fs @ [v])
    1.55 @@ -357,8 +359,8 @@
    1.56  
    1.57          val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
    1.58            |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
    1.59 -               Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
    1.60 -             (case_binder :: ctr_binders) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
    1.61 +              Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
    1.62 +            (case_binder :: ctr_binders) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
    1.63            ||> `Local_Theory.restore;
    1.64  
    1.65          (*transforms defined frees into consts (and more)*)
    1.66 @@ -418,7 +420,7 @@
    1.67                let
    1.68                  val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
    1.69  
    1.70 -                val binder = Binding.suffix_name ("_" ^ suf) b;
    1.71 +                val binder = Binding.suffix_name ("_" ^ suf) fp_b;
    1.72  
    1.73                  val spec =
    1.74                    mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binder, res_T)),
    1.75 @@ -432,8 +434,6 @@
    1.76  
    1.77              val (binders, specs) = map generate_iter_like iter_like_infos |> split_list;
    1.78  
    1.79 -            (* TODO: Allow same constructor (and selector/discriminator) names for different
    1.80 -               types (cf. old "datatype" package) *)
    1.81              val ((csts, defs), (lthy', lthy)) = no_defs_lthy
    1.82                |> apfst split_list o fold_map2 (fn b => fn spec =>
    1.83                  Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
    1.84 @@ -464,7 +464,7 @@
    1.85                let
    1.86                  val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
    1.87  
    1.88 -                val binder = Binding.suffix_name ("_" ^ suf) b;
    1.89 +                val binder = Binding.suffix_name ("_" ^ suf) fp_b;
    1.90  
    1.91                  val spec =
    1.92                    mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
    1.93 @@ -578,7 +578,7 @@
    1.94            |> maps (fn (thmN, thmss, attrs) =>
    1.95              map2 (fn b => fn thms =>
    1.96                ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
    1.97 -                [(thms, [])])) bs thmss);
    1.98 +                [(thms, [])])) fp_bs thmss);
    1.99        in
   1.100          lthy |> Local_Theory.notes notes |> snd
   1.101        end;
   1.102 @@ -676,7 +676,7 @@
   1.103            |> maps (fn (thmN, thmss, attrs) =>
   1.104              map_filter (fn (_, []) => NONE | (b, thms) =>
   1.105                SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
   1.106 -                [(thms, [])])) (bs ~~ thmss));
   1.107 +                [(thms, [])])) (fp_bs ~~ thmss));
   1.108        in
   1.109          lthy |> Local_Theory.notes notes |> snd
   1.110        end;
   1.111 @@ -685,7 +685,7 @@
   1.112        fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list11
   1.113  
   1.114      val lthy' = lthy
   1.115 -      |> fold_map define_ctrs_case_for_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
   1.116 +      |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
   1.117          fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~
   1.118          ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss ~~ raw_sel_defaultsss)
   1.119        |>> split_list |> wrap_types_and_define_iter_likes

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 12 00:20:37 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 12 00:55:11 2012 +0200
     2.3 @@ -98,7 +98,7 @@
     2.4        pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
     2.5  
     2.6      val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0));
     2.7 -    val b = Binding.qualified_name dataT_name;
     2.8 +    val data_b = Binding.qualified_name dataT_name;
     2.9  
    2.10      val (As, B) =
    2.11        no_defs_lthy
    2.12 @@ -120,17 +120,19 @@
    2.13      fun can_omit_disc_binder k m =
    2.14        n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k));
    2.15  
    2.16 -    val std_disc_binder = Binding.name o prefix isN o base_name_of_ctr;
    2.17 +    val std_disc_binder =
    2.18 +      Binding.qualify false (Binding.name_of data_b) o Binding.name o prefix isN o base_name_of_ctr;
    2.19  
    2.20      val disc_binders =
    2.21        raw_disc_binders'
    2.22        |> map4 (fn k => fn m => fn ctr => fn disc =>
    2.23 -        if Binding.eq_name (disc, no_binder) then
    2.24 -          if can_omit_disc_binder k m then NONE else SOME (std_disc_binder ctr)
    2.25 -        else if Binding.eq_name (disc, std_binder) then
    2.26 -          SOME (std_disc_binder ctr)
    2.27 -        else
    2.28 -          SOME disc) ks ms ctrs0;
    2.29 +        Option.map (Binding.qualify false (Binding.name_of data_b))
    2.30 +          (if Binding.eq_name (disc, no_binder) then
    2.31 +             if can_omit_disc_binder k m then NONE else SOME (std_disc_binder ctr)
    2.32 +           else if Binding.eq_name (disc, std_binder) then
    2.33 +             SOME (std_disc_binder ctr)
    2.34 +           else
    2.35 +             SOME disc)) ks ms ctrs0;
    2.36  
    2.37      val no_discs = map is_none disc_binders;
    2.38      val no_discs_at_all = forall I no_discs;
    2.39 @@ -140,10 +142,11 @@
    2.40      val sel_binderss =
    2.41        pad_list [] n raw_sel_binderss
    2.42        |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
    2.43 -        if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, std_binder) then
    2.44 -          std_sel_binder m l ctr
    2.45 -        else
    2.46 -          sel) (1 upto m) o pad_list no_binder m) ctrs0 ms;
    2.47 +        Binding.qualify false (Binding.name_of data_b)
    2.48 +          (if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, std_binder) then
    2.49 +            std_sel_binder m l ctr
    2.50 +          else
    2.51 +            sel)) (1 upto m) o pad_list no_binder m) ctrs0 ms;
    2.52  
    2.53      fun mk_case Ts T =
    2.54        let
    2.55 @@ -571,7 +574,8 @@
    2.56             (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
    2.57            |> filter_out (null o #2)
    2.58            |> map (fn (thmN, thms, attrs) =>
    2.59 -            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), [(thms, [])]));
    2.60 +            ((Binding.qualify true (Binding.name_of data_b) (Binding.name thmN), attrs),
    2.61 +             [(thms, [])]));
    2.62  
    2.63          val notes' =
    2.64            [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]