src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55342 1bd9e637ac9f
parent 54970 891141de5672
child 55347 a87e49f4336d
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 05 23:30:02 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Feb 06 00:03:12 2014 +0100
     1.3 @@ -205,12 +205,9 @@
     1.4  fun mk_half_pairss p = mk_half_pairss' [[]] p;
     1.5  
     1.6  fun join_halves n half_xss other_half_xss =
     1.7 -  let
     1.8 -    val xsss =
     1.9 -      map2 (map2 append) (Library.chop_groups n half_xss)
    1.10 -        (transpose (Library.chop_groups n other_half_xss))
    1.11 -    val xs = splice (flat half_xss) (flat other_half_xss);
    1.12 -  in (xs, xsss) end;
    1.13 +  (splice (flat half_xss) (flat other_half_xss),
    1.14 +   map2 (map2 append) (Library.chop_groups n half_xss)
    1.15 +     (transpose (Library.chop_groups n other_half_xss)));
    1.16  
    1.17  fun mk_undefined T = Const (@{const_name undefined}, T);
    1.18  
    1.19 @@ -252,9 +249,7 @@
    1.20  val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
    1.21  
    1.22  fun dest_ctr ctxt s t =
    1.23 -  let
    1.24 -    val (f, args) = Term.strip_comb t;
    1.25 -  in
    1.26 +  let val (f, args) = Term.strip_comb t in
    1.27      (case ctr_sugar_of ctxt s of
    1.28        SOME {ctrs, ...} =>
    1.29        (case find_first (can (fo_match ctxt f)) ctrs of