--- a/src/HOL/Tools/datatype_case.ML Sat May 17 14:27:02 2008 +0200
+++ b/src/HOL/Tools/datatype_case.ML Sat May 17 15:31:42 2008 +0200
@@ -291,7 +291,7 @@
[] => ()
| is => (if err then case_error else warning)
("The following clauses are redundant (covered by preceding clauses):\n" ^
- space_implode "\n" (map (string_of_clause o nth clauses) is));
+ cat_lines (map (string_of_clause o nth clauses) is));
in
(case_tm, patts2)
end;
--- a/src/HOL/Tools/inductive_codegen.ML Sat May 17 14:27:02 2008 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Sat May 17 15:31:42 2008 +0200
@@ -126,7 +126,7 @@
(iss @ [SOME is]));
fun print_modes modes = message ("Inferred modes:\n" ^
- space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map
+ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
string_of_mode ms)) modes));
val term_vs = map (fst o fst o dest_Var) o term_vars;
@@ -471,7 +471,7 @@
(Graph.all_preds (fst gr) [dep]))));
fun print_arities arities = message ("Arities:\n" ^
- space_implode "\n" (map (fn (s, (ks, k)) => s ^ ": " ^
+ cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
space_implode " -> " (map
(fn NONE => "X" | SOME k' => string_of_int k')
(ks @ [SOME k]))) arities));
--- a/src/HOL/Tools/meson.ML Sat May 17 14:27:02 2008 +0200
+++ b/src/HOL/Tools/meson.ML Sat May 17 15:31:42 2008 +0200
@@ -625,9 +625,9 @@
let val horns = make_horns (cls@ths)
val _ =
Output.debug (fn () => ("meson method called:\n" ^
- space_implode "\n" (map Display.string_of_thm (cls@ths)) ^
+ cat_lines (map Display.string_of_thm (cls@ths)) ^
"\nclauses:\n" ^
- space_implode "\n" (map Display.string_of_thm horns)))
+ cat_lines (map Display.string_of_thm horns)))
in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
end
);
--- a/src/HOL/Tools/metis_tools.ML Sat May 17 14:27:02 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML Sat May 17 15:31:42 2008 +0200
@@ -230,9 +230,9 @@
else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
" but gets " ^ Int.toString (length tys) ^
" type arguments\n" ^
- space_implode "\n" (map (Syntax.string_of_typ ctxt) tys) ^
+ cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
" the terms are \n" ^
- space_implode "\n" (map (Syntax.string_of_term ctxt) (terms_of tts)))
+ cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
case Recon.strip_prefix ResClause.tconst_prefix a of
--- a/src/HOL/Tools/refute.ML Sat May 17 14:27:02 2008 +0200
+++ b/src/HOL/Tools/refute.ML Sat May 17 15:31:42 2008 +0200
@@ -263,7 +263,7 @@
if null terms then
"empty interpretation (no free variables in term)\n"
else
- space_implode "\n" (List.mapPartial (fn (t, intr) =>
+ cat_lines (List.mapPartial (fn (t, intr) =>
(* print constants only if 'show_consts' is true *)
if (!show_consts) orelse not (is_Const t) then
SOME (Sign.string_of_term thy t ^ ": " ^
--- a/src/HOL/Tools/refute_isar.ML Sat May 17 14:27:02 2008 +0200
+++ b/src/HOL/Tools/refute_isar.ML Sat May 17 15:31:42 2008 +0200
@@ -87,7 +87,7 @@
val output = if new_default_params=[] then
"none"
else
- space_implode "\n" (map (fn (name, value) => name ^ "=" ^ value)
+ cat_lines (map (fn (name, value) => name ^ "=" ^ value)
new_default_params)
in
writeln ("Default parameters for 'refute':\n" ^ output);
--- a/src/HOL/Tools/sat_funcs.ML Sat May 17 14:27:02 2008 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Sat May 17 15:31:42 2008 +0200
@@ -325,12 +325,12 @@
(* sorted in ascending order *)
val sorted_clauses = sort (Term.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
val _ = if !trace_sat then
- tracing ("Sorted non-trivial clauses:\n" ^ space_implode "\n" (map Display.string_of_cterm sorted_clauses))
+ tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
else ()
(* translate clauses from HOL terms to PropLogic.prop_formula *)
val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty
val _ = if !trace_sat then
- tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms))
+ tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
else ()
val fm = PropLogic.all fms
(* unit -> Thm.thm *)
--- a/src/HOL/Tools/watcher.ML Sat May 17 14:27:02 2008 +0200
+++ b/src/HOL/Tools/watcher.ML Sat May 17 15:31:42 2008 +0200
@@ -346,7 +346,7 @@
Display.string_of_cterm (List.nth(cprems_of th, i-1))
handle Subscript => "Subgoal number out of range!"
-fun prems_string_of th = space_implode "\n" (map Display.string_of_cterm (cprems_of th))
+fun prems_string_of th = cat_lines (map Display.string_of_cterm (cprems_of th))
fun read_proof probfile =
let val p = ResReconstruct.txt_path probfile
--- a/src/Pure/codegen.ML Sat May 17 14:27:02 2008 +0200
+++ b/src/Pure/codegen.ML Sat May 17 15:31:42 2008 +0200
@@ -699,7 +699,7 @@
NONE => (case get_aux_code aux of
[] => (gr4, p module)
| xs => (add_edge (node_id, dep) (new_node
- (node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr4),
+ (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4),
p module'))
| SOME (_, module'', _) =>
(add_edge (node_id, dep) gr4, p module''))
@@ -780,7 +780,7 @@
[] => (gr'', p module')
| xs => (fst (mk_type_id module' s
(add_edge (node_id, dep) (new_node (node_id,
- (NONE, module', space_implode "\n" xs ^ "\n")) gr''))),
+ (NONE, module', cat_lines xs ^ "\n")) gr''))),
p module'))
| SOME (_, module'', _) =>
(add_edge (node_id, dep) gr'', p module''))
@@ -943,7 +943,7 @@
val (code, gr) = setmp mode ["term_of", "test"]
(generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
val s = PrintMode.setmp [] (fn () => "structure TestTerm =\nstruct\n\n" ^
- space_implode "\n" (map snd code) ^
+ cat_lines (map snd code) ^
"\nopen Generated;\n\n" ^ Pretty.string_of
(Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1,
@@ -1044,7 +1044,7 @@
(generate_code_i thy [] "Generated")
[("result", Abs ("x", TFree ("'a", []), t))];
val s = "structure EvalTerm =\nstruct\n\n" ^
- space_implode "\n" (map snd code) ^
+ cat_lines (map snd code) ^
"\nopen Generated;\n\n" ^ Pretty.string_of
(Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>",
Pretty.brk 1,
@@ -1149,7 +1149,7 @@
in ((case opt_fname of
NONE =>
ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none
- (space_implode "\n" (map snd code))
+ (cat_lines (map snd code))
| SOME fname =>
if lib then
app (fn (name, s) => File.write
--- a/src/Tools/nbe.ML Sat May 17 14:27:02 2008 +0200
+++ b/src/Tools/nbe.ML Sat May 17 15:31:42 2008 +0200
@@ -103,7 +103,7 @@
in space_implode "\n | " (map eqn eqs) end;
in
(prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss
- |> space_implode "\n"
+ |> cat_lines
|> suffix "\n"
end;