src/Tools/Compute_Oracle/am_sml.ML

 	     in
 		 if a <= len then 
 		     let
 			 val strict_a = (case toplevel_arity_of c of SOME sa => sa | NONE => a)
 			 val _ = if strict_a > a then raise Compile "strict" else ()
-			 val s = module_prefix^"c"^(str c)^(concat (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a))))
-			 val s = s^(concat (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a))))
+			 val s = module_prefix^"c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a))))
+			 val s = s^(implode (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a))))
 		     in
 			 print_apps d s (List.drop (args, a))
 		     end
 		 else 
 		     let

 	val c = (case p of PConst (c, _) => c | _ => raise Match)
 	val (n, pattern) = print_pattern true 0 p
 	val lazy_vars = the (arity_of c) - the (toplevel_arity_of c)
 	fun print_tm tm = print_term NONE arity_of toplevel_arity_of n lazy_vars tm
         fun print_guard (Guard (a,b)) = "term_eq ("^(print_tm a)^") ("^(print_tm b)^")"
-	val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(concat (map (fn i => " a"^(str i)) (section (the (arity_of c)))))
+	val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(implode (map (fn i => " a"^(str i)) (section (the (arity_of c)))))
 	fun print_guards t [] = print_tm t
-	  | print_guards t (g::gs) = "if ("^(print_guard g)^")"^(concat (map (fn g => " andalso ("^(print_guard g)^")") gs))^" then ("^(print_tm t)^") else "^else_branch
+	  | print_guards t (g::gs) = "if ("^(print_guard g)^")"^(implode (map (fn g => " andalso ("^(print_guard g)^")") gs))^" then ("^(print_tm t)^") else "^else_branch
     in
 	(if null guards then gnum else gnum+1, pattern^" = "^(print_guards t guards))
     end
 
 fun group_rules rules =

 	val (arity, toplevel_arity, rules) = adjust_rules rules
 	val rules = group_rules rules
 	val constants = Inttab.keys arity
 	fun arity_of c = Inttab.lookup arity c
 	fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
-	fun rep_str s n = concat (rep n s)
+	fun rep_str s n = implode (rep n s)
 	fun indexed s n = s^(str n)
         fun string_of_tuple [] = ""
-	  | string_of_tuple (x::xs) = "("^x^(concat (map (fn s => ", "^s) xs))^")"
+	  | string_of_tuple (x::xs) = "("^x^(implode (map (fn s => ", "^s) xs))^")"
         fun string_of_args [] = ""
-	  | string_of_args (x::xs) = x^(concat (map (fn s => " "^s) xs))
+	  | string_of_args (x::xs) = x^(implode (map (fn s => " "^s) xs))
 	fun default_case gnum c = 
 	    let
-		val leftargs = concat (map (indexed " x") (section (the (arity_of c))))
+		val leftargs = implode (map (indexed " x") (section (the (arity_of c))))
 		val rightargs = section (the (arity_of c))
 		val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa)
 		val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs
 		val right = (indexed "C" c)^" "^(string_of_tuple xs)
 		val message = "(\"unresolved lazy call: " ^ string_of_int c ^ "\")"

 	fun mk_constr_type_args n = if n > 0 then " of Term "^(rep_str " * Term" (n-1)) else ""
 	val _ = writelist [                   
 		"structure "^name^" = struct",
 		"",
 		"datatype Term = Const of int | App of Term * Term | Abs of (Term -> Term)",
-		"         "^(concat (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)),
+		"         "^(implode (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)),
 		""]
 	fun make_constr c argprefix = "(C"^(str c)^" "^(string_of_tuple (map (fn i => argprefix^(str i)) (section (the (arity_of c)))))^")"
 	fun make_term_eq c = "  | term_eq "^(make_constr c "a")^" "^(make_constr c "b")^" = "^
                              (case the (arity_of c) of 
 				  0 => "true"
 				| n => 
 				  let 
 				      val eqs = map (fn i => "term_eq a"^(str i)^" b"^(str i)) (section n)
 				      val (eq, eqs) = (List.hd eqs, map (fn s => " andalso "^s) (List.tl eqs))
 				  in
-				      eq^(concat eqs)
+				      eq^(implode eqs)
 				  end)
 	val _ = writelist [
 		"fun term_eq (Const c1) (Const c2) = (c1 = c2)",
 		"  | term_eq (App (a1,a2)) (App (b1,b2)) = term_eq a1 b1 andalso term_eq a2 b2"]
 	val _ = writelist (map make_term_eq constants)		

 						in 
 						    if gnum' = gnum then 
 							(gnum, r::l)::rs
 						    else
 							let
-							    val args = concat (map (fn i => " a"^(str i)) (section (the (arity_of c))))
+							    val args = implode (map (fn i => " a"^(str i)) (section (the (arity_of c))))
 							    fun gnumc g = if g > 0 then "c"^(str c)^"_"^(str g)^args else "c"^(str c)^args
 							    val s = gnumc (gnum) ^ " = " ^ gnumc (gnum') 
 							in
 							    (gnum', [])::(gnum, s::r::l)::rs
 							end

 	    let
 		val args = map (indexed "a") (section (the (arity_of c)))
 		val leftargs = 
 		    case args of
 			[] => ""
-		      | (x::xs) => "("^x^(concat (map (fn s => ", "^s) xs))^")"
+		      | (x::xs) => "("^x^(implode (map (fn s => ", "^s) xs))^")"
 		val args = map (indexed "convert a") (section (the (arity_of c)))
 		val right = fold (fn x => fn s => "AM_SML.App ("^s^", "^x^")") args ("AM_SML.Const "^(str c))
 	    in
 		"  | convert (C"^(str c)^" "^leftargs^") = "^right
 	    end