# HG changeset patch # User blanchet # Date 1392360826 -3600 # Node ID 46e6e1d91056f601ccb303203640e3361f4e0c78 # Parent b19dd108f0c228cf7ef14db2ecf26c4a61acf738 removed needless robustness (no longer needed thanks to new syntax) diff -r b19dd108f0c2 -r 46e6e1d91056 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Feb 14 07:53:46 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Feb 14 07:53:46 2014 +0100 @@ -308,8 +308,7 @@ val _ = if n > 0 then () else error "No constructors specified"; val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; - val sel_defaultss = - pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss); + val sel_defaultss = map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss; val Type (fcT_name, As0) = body_type (fastype_of (hd ctrs0)); val fc_b_name = Long_Name.base_name fcT_name; @@ -334,9 +333,7 @@ val ms = map length ctr_Tss; - val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings; - - fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings' (k - 1))); + fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings (k - 1))); fun can_rely_on_disc k = can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2)); fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k)); @@ -347,7 +344,7 @@ val standard_disc_binding = Binding.name o prefix isN o base_name_of_ctr; val disc_bindings = - raw_disc_bindings' + raw_disc_bindings |> map4 (fn k => fn m => fn ctr => fn disc => qualify false (if Binding.is_empty disc then @@ -363,13 +360,12 @@ fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr; val sel_bindingss = - pad_list [] n raw_sel_bindingss - |> map3 (fn ctr => fn m => map2 (fn l => fn sel => + map3 (fn ctr => fn m => map2 (fn l => fn sel => qualify false (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then standard_sel_binding m l ctr else - sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms; + sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms raw_sel_bindingss; val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;