1.1 --- a/src/HOL/Tools/datatype_case.ML Sat May 17 14:27:02 2008 +0200
1.2 +++ b/src/HOL/Tools/datatype_case.ML Sat May 17 15:31:42 2008 +0200
1.3 @@ -291,7 +291,7 @@
1.4 [] => ()
1.5 | is => (if err then case_error else warning)
1.6 ("The following clauses are redundant (covered by preceding clauses):\n" ^
1.7 - space_implode "\n" (map (string_of_clause o nth clauses) is));
1.8 + cat_lines (map (string_of_clause o nth clauses) is));
1.9 in
1.10 (case_tm, patts2)
1.11 end;
2.1 --- a/src/HOL/Tools/inductive_codegen.ML Sat May 17 14:27:02 2008 +0200
2.2 +++ b/src/HOL/Tools/inductive_codegen.ML Sat May 17 15:31:42 2008 +0200
2.3 @@ -126,7 +126,7 @@
2.4 (iss @ [SOME is]));
2.5
2.6 fun print_modes modes = message ("Inferred modes:\n" ^
2.7 - space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map
2.8 + cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
2.9 string_of_mode ms)) modes));
2.10
2.11 val term_vs = map (fst o fst o dest_Var) o term_vars;
2.12 @@ -471,7 +471,7 @@
2.13 (Graph.all_preds (fst gr) [dep]))));
2.14
2.15 fun print_arities arities = message ("Arities:\n" ^
2.16 - space_implode "\n" (map (fn (s, (ks, k)) => s ^ ": " ^
2.17 + cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
2.18 space_implode " -> " (map
2.19 (fn NONE => "X" | SOME k' => string_of_int k')
2.20 (ks @ [SOME k]))) arities));
3.1 --- a/src/HOL/Tools/meson.ML Sat May 17 14:27:02 2008 +0200
3.2 +++ b/src/HOL/Tools/meson.ML Sat May 17 15:31:42 2008 +0200
3.3 @@ -625,9 +625,9 @@
3.4 let val horns = make_horns (cls@ths)
3.5 val _ =
3.6 Output.debug (fn () => ("meson method called:\n" ^
3.7 - space_implode "\n" (map Display.string_of_thm (cls@ths)) ^
3.8 + cat_lines (map Display.string_of_thm (cls@ths)) ^
3.9 "\nclauses:\n" ^
3.10 - space_implode "\n" (map Display.string_of_thm horns)))
3.11 + cat_lines (map Display.string_of_thm horns)))
3.12 in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
3.13 end
3.14 );
4.1 --- a/src/HOL/Tools/metis_tools.ML Sat May 17 14:27:02 2008 +0200
4.2 +++ b/src/HOL/Tools/metis_tools.ML Sat May 17 15:31:42 2008 +0200
4.3 @@ -230,9 +230,9 @@
4.4 else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
4.5 " but gets " ^ Int.toString (length tys) ^
4.6 " type arguments\n" ^
4.7 - space_implode "\n" (map (Syntax.string_of_typ ctxt) tys) ^
4.8 + cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
4.9 " the terms are \n" ^
4.10 - space_implode "\n" (map (Syntax.string_of_term ctxt) (terms_of tts)))
4.11 + cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
4.12 end
4.13 | NONE => (*Not a constant. Is it a type constructor?*)
4.14 case Recon.strip_prefix ResClause.tconst_prefix a of
5.1 --- a/src/HOL/Tools/refute.ML Sat May 17 14:27:02 2008 +0200
5.2 +++ b/src/HOL/Tools/refute.ML Sat May 17 15:31:42 2008 +0200
5.3 @@ -263,7 +263,7 @@
5.4 if null terms then
5.5 "empty interpretation (no free variables in term)\n"
5.6 else
5.7 - space_implode "\n" (List.mapPartial (fn (t, intr) =>
5.8 + cat_lines (List.mapPartial (fn (t, intr) =>
5.9 (* print constants only if 'show_consts' is true *)
5.10 if (!show_consts) orelse not (is_Const t) then
5.11 SOME (Sign.string_of_term thy t ^ ": " ^
6.1 --- a/src/HOL/Tools/refute_isar.ML Sat May 17 14:27:02 2008 +0200
6.2 +++ b/src/HOL/Tools/refute_isar.ML Sat May 17 15:31:42 2008 +0200
6.3 @@ -87,7 +87,7 @@
6.4 val output = if new_default_params=[] then
6.5 "none"
6.6 else
6.7 - space_implode "\n" (map (fn (name, value) => name ^ "=" ^ value)
6.8 + cat_lines (map (fn (name, value) => name ^ "=" ^ value)
6.9 new_default_params)
6.10 in
6.11 writeln ("Default parameters for 'refute':\n" ^ output);
7.1 --- a/src/HOL/Tools/sat_funcs.ML Sat May 17 14:27:02 2008 +0200
7.2 +++ b/src/HOL/Tools/sat_funcs.ML Sat May 17 15:31:42 2008 +0200
7.3 @@ -325,12 +325,12 @@
7.4 (* sorted in ascending order *)
7.5 val sorted_clauses = sort (Term.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
7.6 val _ = if !trace_sat then
7.7 - tracing ("Sorted non-trivial clauses:\n" ^ space_implode "\n" (map Display.string_of_cterm sorted_clauses))
7.8 + tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
7.9 else ()
7.10 (* translate clauses from HOL terms to PropLogic.prop_formula *)
7.11 val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty
7.12 val _ = if !trace_sat then
7.13 - tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms))
7.14 + tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
7.15 else ()
7.16 val fm = PropLogic.all fms
7.17 (* unit -> Thm.thm *)
8.1 --- a/src/HOL/Tools/watcher.ML Sat May 17 14:27:02 2008 +0200
8.2 +++ b/src/HOL/Tools/watcher.ML Sat May 17 15:31:42 2008 +0200
8.3 @@ -346,7 +346,7 @@
8.4 Display.string_of_cterm (List.nth(cprems_of th, i-1))
8.5 handle Subscript => "Subgoal number out of range!"
8.6
8.7 -fun prems_string_of th = space_implode "\n" (map Display.string_of_cterm (cprems_of th))
8.8 +fun prems_string_of th = cat_lines (map Display.string_of_cterm (cprems_of th))
8.9
8.10 fun read_proof probfile =
8.11 let val p = ResReconstruct.txt_path probfile
9.1 --- a/src/Pure/codegen.ML Sat May 17 14:27:02 2008 +0200
9.2 +++ b/src/Pure/codegen.ML Sat May 17 15:31:42 2008 +0200
9.3 @@ -699,7 +699,7 @@
9.4 NONE => (case get_aux_code aux of
9.5 [] => (gr4, p module)
9.6 | xs => (add_edge (node_id, dep) (new_node
9.7 - (node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr4),
9.8 + (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4),
9.9 p module'))
9.10 | SOME (_, module'', _) =>
9.11 (add_edge (node_id, dep) gr4, p module''))
9.12 @@ -780,7 +780,7 @@
9.13 [] => (gr'', p module')
9.14 | xs => (fst (mk_type_id module' s
9.15 (add_edge (node_id, dep) (new_node (node_id,
9.16 - (NONE, module', space_implode "\n" xs ^ "\n")) gr''))),
9.17 + (NONE, module', cat_lines xs ^ "\n")) gr''))),
9.18 p module'))
9.19 | SOME (_, module'', _) =>
9.20 (add_edge (node_id, dep) gr'', p module''))
9.21 @@ -943,7 +943,7 @@
9.22 val (code, gr) = setmp mode ["term_of", "test"]
9.23 (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
9.24 val s = PrintMode.setmp [] (fn () => "structure TestTerm =\nstruct\n\n" ^
9.25 - space_implode "\n" (map snd code) ^
9.26 + cat_lines (map snd code) ^
9.27 "\nopen Generated;\n\n" ^ Pretty.string_of
9.28 (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
9.29 Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1,
9.30 @@ -1044,7 +1044,7 @@
9.31 (generate_code_i thy [] "Generated")
9.32 [("result", Abs ("x", TFree ("'a", []), t))];
9.33 val s = "structure EvalTerm =\nstruct\n\n" ^
9.34 - space_implode "\n" (map snd code) ^
9.35 + cat_lines (map snd code) ^
9.36 "\nopen Generated;\n\n" ^ Pretty.string_of
9.37 (Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>",
9.38 Pretty.brk 1,
9.39 @@ -1149,7 +1149,7 @@
9.40 in ((case opt_fname of
9.41 NONE =>
9.42 ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none
9.43 - (space_implode "\n" (map snd code))
9.44 + (cat_lines (map snd code))
9.45 | SOME fname =>
9.46 if lib then
9.47 app (fn (name, s) => File.write
10.1 --- a/src/Tools/nbe.ML Sat May 17 14:27:02 2008 +0200
10.2 +++ b/src/Tools/nbe.ML Sat May 17 15:31:42 2008 +0200
10.3 @@ -103,7 +103,7 @@
10.4 in space_implode "\n | " (map eqn eqs) end;
10.5 in
10.6 (prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss
10.7 - |> space_implode "\n"
10.8 + |> cat_lines
10.9 |> suffix "\n"
10.10 end;
10.11