--- a/src/HOL/Import/hol4rews.ML Sun Jun 20 09:28:35 2004 +0200
+++ b/src/HOL/Import/hol4rews.ML Sun Jun 20 09:30:12 2004 +0200
@@ -650,7 +650,7 @@
val _ = app (fn (hol,(internal,isa,opt_ty)) =>
(out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
case opt_ty of
- Some ty => out (" :: \"" ^ (Output.output (string_of_ctyp (ctyp_of sg ty))) ^ "\"")
+ Some ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of sg ty)) ^ "\"")
| None => ())) constmaps
val _ = if null constmaps
then ()
--- a/src/HOL/Import/proof_kernel.ML Sun Jun 20 09:28:35 2004 +0200
+++ b/src/HOL/Import/proof_kernel.ML Sun Jun 20 09:30:12 2004 +0200
@@ -190,7 +190,7 @@
| G _ = error ("ProofKernel.smart_string_of_cterm internal error: " ^ (G 2 string_of_cterm ct))
fun F sh_br n =
let
- val str = Library.setmp show_brackets sh_br (G n (Output.output o string_of_cterm)) ct
+ val str = Library.setmp show_brackets sh_br (G n string_of_cterm) ct
val cu = transform_error (read_cterm sign) (str,T)
in
if match cu
@@ -208,7 +208,7 @@
handle ERROR_MESSAGE mesg =>
(writeln "Exception in smart_string_of_cterm!";
writeln mesg;
- quote (Output.output (string_of_cterm ct)))
+ quote (string_of_cterm ct))
val smart_string_of_thm = smart_string_of_cterm o cprop_of
@@ -1898,9 +1898,9 @@
val crhs = cterm_of sg (#2 (Logic.dest_equals (prop_of rew)))
val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
then
- add_dump ("constdefs\n " ^ (quotename constname) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg ctype)) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n " ^ (smart_string_of_cterm crhs)) thy''
+ add_dump ("constdefs\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg ctype) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n " ^ (smart_string_of_cterm crhs)) thy''
else
- add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg ctype)) ^
+ add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg ctype) ^
"\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
thy''
@@ -1964,7 +1964,7 @@
end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
val sg = sign_of thy
val str = foldl (fn (acc,(c,T,csyn)) =>
- acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg T)) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
+ acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg T) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
val thy' = add_dump str thy
in
Theory.add_consts_i consts thy'
--- a/src/HOL/Modelcheck/MuCalculus.ML Sun Jun 20 09:28:35 2004 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.ML Sun Jun 20 09:30:12 2004 +0200
@@ -13,7 +13,7 @@
local
fun termtext sign term =
- setmp print_mode ["Eindhoven"] (Output.output o Sign.string_of_term sign) term;
+ setmp print_mode ["Eindhoven"] (Sign.string_of_term sign) term;
fun call_mc s =
execute ( "echo \"" ^ s ^ "\" | pmu -w" );
--- a/src/HOL/Modelcheck/mucke_oracle.ML Sun Jun 20 09:28:35 2004 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Sun Jun 20 09:30:12 2004 +0200
@@ -487,7 +487,7 @@
fun string_of_terms sign terms =
let fun make_string sign [] = "" |
make_string sign (trm::list) =
- ((Output.output (Sign.string_of_term sign trm)) ^ "\n" ^(make_string sign list))
+ Sign.string_of_term sign trm ^ "\n" ^ make_string sign list
in
(setmp print_mode ["Mucke"] (make_string sign) terms)
end;
--- a/src/Pure/codegen.ML Sun Jun 20 09:28:35 2004 +0200
+++ b/src/Pure/codegen.ML Sun Jun 20 09:30:12 2004 +0200
@@ -471,11 +471,11 @@
(Graph.new_node (id, (None, "")) gr'), rhs');
val (gr2, xs) = codegens false (gr1, args');
val (gr3, ty) = invoke_tycodegen thy id false (gr2, T);
- in Graph.map_node id (K (None, Output.output (Pretty.string_of (Pretty.block
+ in Graph.map_node id (K (None, Pretty.string_of (Pretty.block
(separate (Pretty.brk 1) (if null args' then
[Pretty.str ("val " ^ id ^ " :"), ty]
else Pretty.str ("fun " ^ id) :: xs) @
- [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n"))) gr3
+ [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr3
end, mk_app brack (Pretty.str id) ps)
end))
@@ -527,7 +527,7 @@
space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
[Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
"\n\nend;\n\nopen Generated;\n";
- in Output.output code end));
+ in code end));
val generate_code_i = gen_generate_code (K I);
val generate_code = gen_generate_code
@@ -581,7 +581,7 @@
val s = "structure TestTerm =\nstruct\n\n" ^
setmp mode ["term_of", "test"] (generate_code_i thy)
[("testf", list_abs_free (frees, t))] ^
- "\n" ^ Output.output (Pretty.string_of
+ "\n" ^ Pretty.string_of
(Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1,
Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
@@ -601,7 +601,7 @@
mk_app false (mk_term_of sg false T)
[Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @
[Pretty.str "]"])]],
- Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"])) ^
+ Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
"\n\nend;\n";
val _ = use_text Context.ml_output false s;
fun iter f k = if k > i then None