src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55470 46e6e1d91056
parent 55469 b19dd108f0c2
child 55471 198498f861ee
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -308,8 +308,7 @@
     1.4      val _ = if n > 0 then () else error "No constructors specified";
     1.5  
     1.6      val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
     1.7 -    val sel_defaultss =
     1.8 -      pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
     1.9 +    val sel_defaultss = map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss;
    1.10  
    1.11      val Type (fcT_name, As0) = body_type (fastype_of (hd ctrs0));
    1.12      val fc_b_name = Long_Name.base_name fcT_name;
    1.13 @@ -334,9 +333,7 @@
    1.14  
    1.15      val ms = map length ctr_Tss;
    1.16  
    1.17 -    val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
    1.18 -
    1.19 -    fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
    1.20 +    fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings (k - 1)));
    1.21      fun can_rely_on_disc k =
    1.22        can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
    1.23      fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
    1.24 @@ -347,7 +344,7 @@
    1.25      val standard_disc_binding = Binding.name o prefix isN o base_name_of_ctr;
    1.26  
    1.27      val disc_bindings =
    1.28 -      raw_disc_bindings'
    1.29 +      raw_disc_bindings
    1.30        |> map4 (fn k => fn m => fn ctr => fn disc =>
    1.31          qualify false
    1.32            (if Binding.is_empty disc then
    1.33 @@ -363,13 +360,12 @@
    1.34      fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
    1.35  
    1.36      val sel_bindingss =
    1.37 -      pad_list [] n raw_sel_bindingss
    1.38 -      |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
    1.39 +      map3 (fn ctr => fn m => map2 (fn l => fn sel =>
    1.40          qualify false
    1.41            (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then
    1.42              standard_sel_binding m l ctr
    1.43            else
    1.44 -            sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
    1.45 +            sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms raw_sel_bindingss;
    1.46  
    1.47      val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
    1.48