diff -r 9606c6224933 -r 2c39efba8f67 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Tue Jun 22 10:05:47 2004 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Tue Jun 22 14:14:08 2004 +0200
@@ -88,31 +88,38 @@
 		  | cnf_number_of_clauses _ =
 			1
 		(* prop_formula -> string *)
-		fun cnf_string True =
-			error "formula is not in CNF"
-		  | cnf_string False =
-			error "formula is not in CNF"
-		  | cnf_string (BoolVar i) =
-			(assert (i>=1) "formula contains a variable index less than 1";
-			string_of_int i)
-		  | cnf_string (Not fm) =
-			"-" ^ cnf_string fm
-		  | cnf_string (Or (fm1,fm2)) =
-			cnf_string fm1 ^ " " ^ cnf_string fm2
-		  | cnf_string (And (fm1,fm2)) =
-			cnf_string fm1 ^ " 0\n" ^ cnf_string fm2
+		fun cnf_string fm =
+		let
+			(* prop_formula -> string list -> string list *)
+			fun cnf_string_acc True acc =
+				error "formula is not in CNF"
+			  | cnf_string_acc False acc =
+				error "formula is not in CNF"
+			  | cnf_string_acc (BoolVar i) acc =
+				(assert (i>=1) "formula contains a variable index less than 1";
+				string_of_int i :: acc)
+			  | cnf_string_acc (Not (BoolVar i)) acc =
+				"-" :: cnf_string_acc (BoolVar i) acc
+			  | cnf_string_acc (Not _) acc =
+				error "formula is not in CNF"
+			  | cnf_string_acc (Or (fm1,fm2)) acc =
+				cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc)
+			  | cnf_string_acc (And (fm1,fm2)) acc =
+				cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc)
+		in
+			concat (cnf_string_acc fm [])
+		end
 	in
 		File.write path
 			(let
 				val fm'               = cnf_True_False_elim fm
 				val number_of_vars    = maxidx fm'
 				val number_of_clauses = cnf_number_of_clauses fm'
-				val cnfstring         = cnf_string fm'
 			in
 				"c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
 				"c (c) Tjark Weber\n" ^
 				"p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^
-				cnfstring ^ " 0\n"
+				cnf_string fm' ^ " 0\n"
 			end)
 	end;
 
@@ -128,19 +135,25 @@
 	fun write_dimacs_sat_file path fm =
 	let
 		(* prop_formula -> string *)
-		fun sat_string True =
-			"*()"
-		  | sat_string False =
-			"+()"
-		  | sat_string (BoolVar i) =
-			(assert (i>=1) "formula contains a variable index less than 1";
-			string_of_int i)
-		  | sat_string (Not fm) =
-			"-(" ^ sat_string fm ^ ")"
-		  | sat_string (Or (fm1,fm2)) =
-			"+(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
-		  | sat_string (And (fm1,fm2)) =
-			"*(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
+		fun sat_string fm =
+		let
+			(* prop_formula -> string list -> string list *)
+			fun sat_string_acc True acc =
+				"*()" :: acc
+			  | sat_string_acc False acc =
+				"+()" :: acc
+			  | sat_string_acc (BoolVar i) acc =
+				(assert (i>=1) "formula contains a variable index less than 1";
+				string_of_int i :: acc)
+			  | sat_string_acc (Not fm) acc =
+				"-(" :: sat_string_acc fm (")" :: acc)
+			  | sat_string_acc (Or (fm1,fm2)) acc =
+				"+(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
+			  | sat_string_acc (And (fm1,fm2)) acc =
+				"*(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
+		in
+			concat (sat_string_acc fm [])
+		end
 	in
 		File.write path
 			(let