eliminated redundant Library.multiply;
authorwenzelm
Sat Jul 25 12:43:45 2009 +0200 (2009-07-25)
changeset 32188005f9abae1e3
parent 32187 cca43ca13f4f
child 32189 4086cdd8dd70
eliminated redundant Library.multiply;
src/Pure/library.ML
src/Tools/induct.ML
     1.1 --- a/src/Pure/library.ML	Sat Jul 25 10:31:27 2009 +0200
     1.2 +++ b/src/Pure/library.ML	Sat Jul 25 12:43:45 2009 +0200
     1.3 @@ -109,7 +109,6 @@
     1.4    val split_list: ('a * 'b) list -> 'a list * 'b list
     1.5    val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
     1.6    val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     1.7 -  val multiply: 'a list -> 'a list list -> 'a list list
     1.8    val separate: 'a -> 'a list -> 'a list
     1.9    val surround: 'a -> 'a list -> 'a list
    1.10    val replicate: int -> 'a -> 'a list
    1.11 @@ -552,9 +551,6 @@
    1.12      else rep (n, [])
    1.13    end;
    1.14  
    1.15 -(*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
    1.16 -fun multiply [] _ = []
    1.17 -  | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
    1.18  
    1.19  (* direct product *)
    1.20  
    1.21 @@ -1138,5 +1134,5 @@
    1.22  
    1.23  end;
    1.24  
    1.25 -structure BasicLibrary: BASIC_LIBRARY = Library;
    1.26 -open BasicLibrary;
    1.27 +structure Basic_Library: BASIC_LIBRARY = Library;
    1.28 +open Basic_Library;
     2.1 --- a/src/Tools/induct.ML	Sat Jul 25 10:31:27 2009 +0200
     2.2 +++ b/src/Tools/induct.ML	Sat Jul 25 12:43:45 2009 +0200
     2.3 @@ -568,7 +568,7 @@
     2.4  *)
     2.5  
     2.6  fun get_inductT ctxt insts =
     2.7 -  fold_rev multiply (insts |> map
     2.8 +  fold_rev (map_product cons) (insts |> map
     2.9        ((fn [] => NONE | ts => List.last ts) #>
    2.10          (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
    2.11          find_inductT ctxt)) [[]]