# HG changeset patch
# User webertj
# Date 1110555306 -3600
# Node ID 6fb06b768f678aecf1f9875bd47ded66b93b6621
# Parent  27a706e3a53dc6ea2321996c5b0e6517ce03c94c
code reformatted

diff -r 27a706e3a53d -r 6fb06b768f67 src/HOL/Tools/res_lib.ML
--- a/src/HOL/Tools/res_lib.ML	Fri Mar 11 16:08:21 2005 +0100
+++ b/src/HOL/Tools/res_lib.ML	Fri Mar 11 16:35:06 2005 +0100
@@ -1,124 +1,111 @@
-(*  Author: Jia Meng, Cambridge University Computer Laboratory
-    ID: $Id$
-    Copyright 2004 University of Cambridge
+(*  Title:      HOL/Tools/res_lib.ML
+    Author:     Jia Meng, Cambridge University Computer Laboratory
+    ID:         $Id$
+    Copyright   2004 University of Cambridge
 
-some frequently used functions by files in this directory.
+Some auxiliary functions frequently used by files in this directory.
 *)
 
 signature RES_LIB =
 sig
 
-val flat_noDup : ''a list list -> ''a list
-val list2str_sep : string -> string list -> string
-val list_to_string : string list -> string
-val list_to_string' : string list -> string
-val no_BDD : string -> string
-val no_blanks : string -> string
-val no_blanks_dots : string -> string
-val no_blanks_dots_dashes : string -> string
-val no_dots : string -> string
-val no_rep_add : ''a -> ''a list -> ''a list
-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
-
+	val flat_noDup : ''a list list -> ''a list
+	val list2str_sep : string -> string list -> string
+	val list_to_string : string list -> string
+	val list_to_string' : string list -> string
+	val no_BDD : string -> string
+	val no_blanks : string -> string
+	val no_blanks_dots : string -> string
+	val no_blanks_dots_dashes : string -> string
+	val no_dots : string -> string
+	val no_rep_add : ''a -> ''a list -> ''a list
+	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;
 
 
-
 structure ResLib : RES_LIB =
-
 struct
 
-(*** convert a list of strings into one single string; surrounded by backets ***)
-fun list_to_string strings =
-    let fun str_of [s] = s 
-          | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
-          | str_of _ = ""
-    in
-	"(" ^ str_of strings ^ ")"
-    end;
+	(* convert a list of strings into one single string; surrounded by brackets *)
+	fun list_to_string strings =
+	let
+		fun str_of [s]      = s
+		  | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
+		  | str_of _        = ""
+	in
+		"(" ^ str_of strings ^ ")"
+	end;
 
-fun list_to_string' strings =
-    let fun str_of [s] = s 
-          | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
-          | str_of _ = ""
-    in
-	"[" ^ str_of strings ^ "]"
-    end;
-
-
+	fun list_to_string' strings =
+	let
+		fun str_of [s]      = s
+		  | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
+		  | str_of _        = ""
+	in
+		"[" ^ str_of strings ^ "]"
+	end;
 
-(*** remove some chars (not allowed by TPTP format) from a string ***)
-fun no_blanks " " = "_"
-  | no_blanks c   = c;
+	(* remove some chars (not allowed by TPTP format) from a string *)
+	fun no_blanks " " = "_"
+	  | no_blanks c   = c;
 
-
-fun no_dots "." = "_dot_"
-  | no_dots c   = c;
-
+	fun no_dots "." = "_dot_"
+	  | no_dots c   = c;
 
-fun no_blanks_dots " " = "_"
-  | no_blanks_dots "." = "_dot_"
-  | no_blanks_dots c   = c;
-    
-fun no_blanks_dots_dashes " " = "_"
-  | no_blanks_dots_dashes "." = "_dot_"
-  | no_blanks_dots_dashes "'" = "_da_"
-  | no_blanks_dots_dashes c   = c;
-    
-fun no_BDD cs = implode (map no_blanks_dots_dashes (explode cs));
+	fun no_blanks_dots " " = "_"
+	  | no_blanks_dots "." = "_dot_"
+	  | no_blanks_dots c   = c;
 
+	fun no_blanks_dots_dashes " " = "_"
+	  | no_blanks_dots_dashes "." = "_dot_"
+	  | no_blanks_dots_dashes "'" = "_da_"
+	  | no_blanks_dots_dashes c   = c;
 
+	fun no_BDD cs =
+		implode (map no_blanks_dots_dashes (explode cs));
 
-fun no_rep_add x [] = [x]
-  | no_rep_add x (y :: z) = if (x = y) then (y :: z)
-                             else y :: (no_rep_add x z); 
+	fun no_rep_add x []     = [x]
+	  | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
 
+	fun no_rep_app l1 []     = l1
+	  | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
 
-fun no_rep_app l1 [] = l1
-  | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
- 
+	fun rm_rep []     = []
+	  | rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y);
 
-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 unzip []             =
+		([], [])
+	  | unzip ((x1, y1)::zs) =
+		let
+			val (xs, ys) = unzip zs
+		in
+			(x1::xs, y1::ys)
+		end;
 
-
-fun flat_noDup [] = []
-  | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
-
+	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);
 
-fun list2str_sep delim [] = delim
-  | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
-
-
+	fun list2str_sep delim []      = delim
+	  | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
 
-fun write_strs _ [] = ()
-  | write_strs out (s::ss) = (TextIO.output(out,s);write_strs out ss);
+	fun write_strs _   []      = ()
+	  | write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss);
 
-fun writeln_strs _ [] = ()
-  | writeln_strs out (s::ss) = (TextIO.output(out,s);TextIO.output(out,"\n");writeln_strs out ss);
+	fun writeln_strs _   []      = ()
+	  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
 
-(* pair the first argument with each of the element in the second input list *)
-fun pair_ins x [] = []
-  | pair_ins x (y::ys) = (x,y) :: (pair_ins x ys);
+	(* pair the first argument with each element in the second input list *)
+	fun pair_ins x []      = []
+	  | pair_ins x (y::ys) = (x, y) :: (pair_ins x ys);
 
-
-end;
\ No newline at end of file
+end;