1.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 18 03:33:53 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 18 09:15:53 2012 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  signature BNF_WRAP =
     1.6  sig
     1.7 -  val no_binding: binding
     1.8    val mk_half_pairss: 'a list -> ('a * 'a) list list
     1.9    val mk_ctr: typ list -> term -> term
    1.10    val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    1.11 @@ -45,7 +44,6 @@
    1.12  val split_asmN = "split_asm";
    1.13  val weak_case_cong_thmsN = "weak_case_cong";
    1.14  
    1.15 -val no_binding = @{binding ""};
    1.16  val std_binding = @{binding _};
    1.17  
    1.18  val induct_simp_attrs = @{attributes [induct_simp]};
    1.19 @@ -111,10 +109,11 @@
    1.20  
    1.21      val ms = map length ctr_Tss;
    1.22  
    1.23 -    val raw_disc_bindings' = pad_list no_binding n raw_disc_bindings;
    1.24 +    val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
    1.25  
    1.26      fun can_really_rely_on_disc k =
    1.27 -      not (Binding.eq_name (nth raw_disc_bindings' (k - 1), no_binding)) orelse nth ms (k - 1) = 0;
    1.28 +      not (Binding.eq_name (nth raw_disc_bindings' (k - 1), Binding.empty)) orelse
    1.29 +      nth ms (k - 1) = 0;
    1.30      fun can_rely_on_disc k =
    1.31        can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
    1.32      fun can_omit_disc_binding k m =
    1.33 @@ -127,7 +126,7 @@
    1.34        raw_disc_bindings'
    1.35        |> map4 (fn k => fn m => fn ctr => fn disc =>
    1.36          Option.map (Binding.qualify false (Binding.name_of data_b))
    1.37 -          (if Binding.eq_name (disc, no_binding) then
    1.38 +          (if Binding.eq_name (disc, Binding.empty) then
    1.39               if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr)
    1.40             else if Binding.eq_name (disc, std_binding) then
    1.41               SOME (std_disc_binding ctr)
    1.42 @@ -143,10 +142,10 @@
    1.43        pad_list [] n raw_sel_bindingss
    1.44        |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
    1.45          Binding.qualify false (Binding.name_of data_b)
    1.46 -          (if Binding.eq_name (sel, no_binding) orelse Binding.eq_name (sel, std_binding) then
    1.47 +          (if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then
    1.48              std_sel_binding m l ctr
    1.49            else
    1.50 -            sel)) (1 upto m) o pad_list no_binding m) ctrs0 ms;
    1.51 +            sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
    1.52  
    1.53      fun mk_case Ts T =
    1.54        let