# HG changeset patch
# User wenzelm
# Date 1248518625 -7200
# Node ID 005f9abae1e3a78d04ac9be76a53df65603ee2ae
# Parent  cca43ca13f4fe243ea30fb8aa445853fe9e7aa57
eliminated redundant Library.multiply;

diff -r cca43ca13f4f -r 005f9abae1e3 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Jul 25 10:31:27 2009 +0200
+++ b/src/Pure/library.ML	Sat Jul 25 12:43:45 2009 +0200
@@ -109,7 +109,6 @@
   val split_list: ('a * 'b) list -> 'a list * 'b list
   val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
-  val multiply: 'a list -> 'a list list -> 'a list list
   val separate: 'a -> 'a list -> 'a list
   val surround: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
@@ -552,9 +551,6 @@
     else rep (n, [])
   end;
 
-(*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
-fun multiply [] _ = []
-  | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
 
 (* direct product *)
 
@@ -1138,5 +1134,5 @@
 
 end;
 
-structure BasicLibrary: BASIC_LIBRARY = Library;
-open BasicLibrary;
+structure Basic_Library: BASIC_LIBRARY = Library;
+open Basic_Library;
diff -r cca43ca13f4f -r 005f9abae1e3 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Jul 25 10:31:27 2009 +0200
+++ b/src/Tools/induct.ML	Sat Jul 25 12:43:45 2009 +0200
@@ -568,7 +568,7 @@
 *)
 
 fun get_inductT ctxt insts =
-  fold_rev multiply (insts |> map
+  fold_rev (map_product cons) (insts |> map
       ((fn [] => NONE | ts => List.last ts) #>
         (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
         find_inductT ctxt)) [[]]