# HG changeset patch # User wenzelm # Date 1087716612 -7200 # Node ID 267cc670317ae2b7b04ca5feec049f9691cf399e # Parent 245955f0c5796b93652d3f9399ff00048d1090fe got rid of Output.output for default print mode; diff -r 245955f0c579 -r 267cc670317a src/HOL/Import/hol4rews.ML --- 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 () diff -r 245955f0c579 -r 267cc670317a src/HOL/Import/proof_kernel.ML --- 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' diff -r 245955f0c579 -r 267cc670317a src/HOL/Modelcheck/MuCalculus.ML --- 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" ); diff -r 245955f0c579 -r 267cc670317a src/HOL/Modelcheck/mucke_oracle.ML --- 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; diff -r 245955f0c579 -r 267cc670317a src/Pure/codegen.ML --- 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