diff -r f14ae2432710 -r 9df37a0e935d src/HOL/Tools/res_lib.ML
--- a/src/HOL/Tools/res_lib.ML	Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Tools/res_lib.ML	Tue Apr 19 18:08:44 2005 +0200
@@ -22,10 +22,8 @@
 	val no_rep_app : ''a list -> ''a list -> ''a list
 	val pair_ins : 'a -> 'b list -> ('a * 'b) list
 	val rm_rep : ''a list -> ''a list
-	val unzip : ('a * 'b) list -> 'a list * 'b list
 	val write_strs : TextIO.outstream -> TextIO.vector list -> unit
 	val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
-	val zip : 'a list -> 'b list -> ('a * 'b) list
 
 end;
 
@@ -80,18 +78,6 @@
 	fun rm_rep []     = []
 	  | rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y);
 
-	fun unzip []             =
-		([], [])
-	  | unzip ((x1, y1)::zs) =
-		let
-			val (xs, ys) = unzip zs
-		in
-			(x1::xs, y1::ys)
-		end;
-
-	fun zip []      []      = []
-	  | zip (x::xs) (y::ys) = (x, y)::(zip xs ys);
-
 	fun flat_noDup []     = []
 	  | flat_noDup (x::y) = no_rep_app x (flat_noDup y);