# HG changeset patch # User wenzelm # Date 1294670746 -3600 # Node ID a2ad5b8240510de04096fe0e4bd267654845ca67 # Parent 0f1e411a14481071897adad8fbb24291a11ecaea eliminated Int.toString; diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Import/proof_kernel.ML Mon Jan 10 15:45:46 2011 +0100 @@ -1281,7 +1281,7 @@ val _ = (message "Looking for consts:"; message (commas cs)) val pot_thms = Shuffler.find_potential thy isaconc - val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems") + val _ = message (string_of_int (length pot_thms) ^ " potential theorems") in case Shuffler.set_prop thy isaconc pot_thms of SOME (isaname,th) => diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Import/shuffler.ML Mon Jan 10 15:45:46 2011 +0100 @@ -465,7 +465,7 @@ end | F (Abs(x,xT,t),idx) = let - val x' = "x" ^ Int.toString idx + val x' = "x" ^ string_of_int idx val (t',idx') = F (t,idx+1) in (Abs(x',xT,t'),idx') diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Import/xml.ML --- a/src/HOL/Import/xml.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Import/xml.ML Mon Jan 10 15:45:46 2011 +0100 @@ -53,7 +53,7 @@ | encode "\"" = """ | encode c = c; -fun encode_charref c = "&#" ^ Int.toString (ord c) ^ ";" +fun encode_charref c = "&#" ^ string_of_int (ord c) ^ ";" val text = Library.translate_string encode diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Matrix/Compute_Oracle/am_compiler.ML --- a/src/HOL/Matrix/Compute_Oracle/am_compiler.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Matrix/Compute_Oracle/am_compiler.ML Mon Jan 10 15:45:46 2011 +0100 @@ -30,7 +30,7 @@ fun print_rule (p, t) = let - fun str x = Int.toString x + fun str x = string_of_int x fun print_pattern n PVar = (n+1, "x"^(str n)) | print_pattern n (PConst (c, [])) = (n, "c"^(str c)) | print_pattern n (PConst (c, args)) = @@ -86,7 +86,7 @@ fun writeln s = (write s; write "\n") fun writelist [] = () | writelist (s::ss) = (writeln s; writelist ss) - fun str i = Int.toString i + fun str i = string_of_int i val _ = writelist [ "structure "^name^" = struct", "", diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Matrix/Compute_Oracle/am_ghc.ML --- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Mon Jan 10 15:45:46 2011 +0100 @@ -108,7 +108,7 @@ fun print_rule arity_of (p, t) = let - fun str x = Int.toString x + fun str x = string_of_int x fun print_pattern top n PVar = (n+1, "x"^(str n)) | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c)) | print_pattern top n (PConst (c, args)) = @@ -149,7 +149,7 @@ fun writeln s = (write s; write "\n") fun writelist [] = () | writelist (s::ss) = (writeln s; writelist ss) - fun str i = Int.toString i + fun str i = string_of_int i val (arity, rules) = adjust_rules rules val rules = group_rules rules val constants = Inttab.keys arity @@ -206,7 +206,7 @@ val c = !guid_counter val _ = guid_counter := !guid_counter + 1 in - (Int.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c) + string_of_int (Time.toMicroseconds (Time.now ())) ^ string_of_int c end fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s]))); diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Matrix/Compute_Oracle/am_sml.ML --- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML Mon Jan 10 15:45:46 2011 +0100 @@ -245,7 +245,7 @@ fun print_rule gnum arity_of toplevel_arity_of (guards, p, t) = let - fun str x = Int.toString x + fun str x = string_of_int x fun print_pattern top n PVar = (n+1, "x"^(str n)) | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else "")) | print_pattern top n (PConst (c, args)) = @@ -300,7 +300,7 @@ fun writeln s = (write s; write "\n") fun writelist [] = () | writelist (s::ss) = (writeln s; writelist ss) - fun str i = Int.toString i + fun str i = string_of_int i val (inlinetab, rules) = inline_rules rules val (arity, toplevel_arity, rules) = adjust_rules rules val rules = group_rules rules @@ -486,7 +486,7 @@ val c = !guid_counter val _ = guid_counter := !guid_counter + 1 in - (Int.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c) + string_of_int (Time.toMicroseconds (Time.now ())) ^ string_of_int c end diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Matrix/Compute_Oracle/compute.ML --- a/src/HOL/Matrix/Compute_Oracle/compute.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Matrix/Compute_Oracle/compute.ML Mon Jan 10 15:45:46 2011 +0100 @@ -170,7 +170,7 @@ type naming = int -> string -fun default_naming i = "v_" ^ Int.toString i +fun default_naming i = "v_" ^ string_of_int i datatype computer = Computer of (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Matrix/Cplex_tools.ML --- a/src/HOL/Matrix/Cplex_tools.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Matrix/Cplex_tools.ML Mon Jan 10 15:45:46 2011 +0100 @@ -1134,7 +1134,7 @@ fun solve_glpk prog = let - val name = Int.toString (Time.toMicroseconds (Time.now ())) + val name = string_of_int (Time.toMicroseconds (Time.now ())) val lpname = tmp_file (name^".lp") val resultname = tmp_file (name^".txt") val _ = save_cplexFile lpname prog @@ -1165,7 +1165,7 @@ () end - val name = Int.toString (Time.toMicroseconds (Time.now ())) + val name = string_of_int (Time.toMicroseconds (Time.now ())) val lpname = tmp_file (name^".lp") val resultname = tmp_file (name^".txt") val scriptname = tmp_file (name^".script") @@ -1174,7 +1174,7 @@ val cplex = if cplex_path = "" then "cplex" else cplex_path val _ = write_script scriptname lpname resultname val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null" - val answer = "return code "^(Int.toString (bash command)) + val answer = "return code " ^ string_of_int (bash command) in let val result = load_cplexResult resultname diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Matrix/FloatSparseMatrixBuilder.ML --- a/src/HOL/Matrix/FloatSparseMatrixBuilder.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Matrix/FloatSparseMatrixBuilder.ML Mon Jan 10 15:45:46 2011 +0100 @@ -144,7 +144,7 @@ fun nameof i = let - val s = "x"^(Int.toString i) + val s = "x" ^ string_of_int i val _ = Unsynchronized.change ytable (Inttab.update (i, s)) in s @@ -201,7 +201,7 @@ else case Int.fromString (String.extract(s, 1, NONE)) of SOME i => i | NONE => raise (No_name s) - fun nameof i = "y"^(Int.toString i) + fun nameof i = "y" ^ string_of_int i fun split_numstr s = if String.isPrefix "-" s then (false,String.extract(s, 1, NONE)) diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jan 10 15:45:46 2011 +0100 @@ -365,7 +365,7 @@ Sledgehammer_Isar.default_params ctxt [("verbose", "true"), ("type_sys", type_sys), - ("timeout", Int.toString timeout)] + ("timeout", string_of_int timeout)] val default_max_relevant = Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name val is_built_in_const = @@ -479,7 +479,7 @@ [("provers", prover_name), ("verbose", "true"), ("type_sys", type_sys), - ("timeout", Int.toString timeout)] + ("timeout", string_of_int timeout)] val minimize = Sledgehammer_Minimize.minimize_facts prover_name params true 1 (Sledgehammer_Util.subgoal_count st) diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Mon Jan 10 15:45:46 2011 +0100 @@ -20,7 +20,7 @@ val chained_ths = [] (* a tactic has no chained ths *) val params as {type_sys, relevance_thresholds, max_relevant, ...} = ((if force_full_types then [("full_types", "true")] else []) - @ [("timeout", Int.toString (Time.toSeconds timeout))]) + @ [("timeout", string_of_int (Time.toSeconds timeout))]) (* @ [("overlord", "true")] *) |> Sledgehammer_Isar.default_params ctxt val prover = Sledgehammer_Provers.get_prover ctxt false name diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Jan 10 15:45:46 2011 +0100 @@ -399,10 +399,10 @@ if exec then let val _ = Output.urgent_message ("BEFORE PARTITION OF " ^ - Int.toString (length mutants) ^ " MUTANTS") + string_of_int (length mutants) ^ " MUTANTS") val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants) - val _ = tracing ("AFTER PARTITION (" ^ Int.toString (length execs) ^ - " vs " ^ Int.toString (length noexecs) ^ ")") + val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^ + " vs " ^ string_of_int (length noexecs) ^ ")") in execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs end @@ -468,10 +468,10 @@ (* subentry -> string *) fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno, timeout, error) = - " " ^ mtd_name ^ ": " ^ Int.toString genuine_cex ^ "+ " ^ - Int.toString potential_cex ^ "= " ^ Int.toString no_cex ^ "- " ^ - Int.toString donno ^ "? " ^ Int.toString timeout ^ "T " ^ - Int.toString error ^ "!" + " " ^ mtd_name ^ ": " ^ string_of_int genuine_cex ^ "+ " ^ + string_of_int potential_cex ^ "= " ^ string_of_int no_cex ^ "- " ^ + string_of_int donno ^ "? " ^ string_of_int timeout ^ "T " ^ + string_of_int error ^ "!" (* entry -> string *) fun string_for_entry (thm_name, exec, subentries) = diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Jan 10 15:45:46 2011 +0100 @@ -97,7 +97,7 @@ \% " ^ timestamp () ^ "\n" :: maps (fn (_, []) => [] | (heading, lines) => - "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" :: + "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" :: map (string_for_problem_line use_conjecture_for_hypotheses) lines) problem @@ -138,7 +138,7 @@ fun add j = let val nice_name = nice_prefix ^ - (if j = 0 then "" else "_" ^ Int.toString j) + (if j = 0 then "" else "_" ^ string_of_int j) in case Symtab.lookup (snd the_pool) nice_name of SOME full_name' => diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jan 10 15:45:46 2011 +0100 @@ -58,7 +58,7 @@ in if length trands = nargs then SomeTerm (list_comb(rator, trands)) else raise Fail ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ - " expected " ^ Int.toString nargs ^ + " expected " ^ string_of_int nargs ^ " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) end; @@ -139,8 +139,8 @@ in if length tys = ntypes then apply_list t nterms (List.drop(tts,ntypes)) else - raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ - " but gets " ^ Int.toString (length tys) ^ + raise Fail ("Constant " ^ c ^ " expects " ^ string_of_int ntypes ^ + " but gets " ^ string_of_int (length tys) ^ " type arguments\n" ^ cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ " the terms are \n" ^ @@ -407,11 +407,11 @@ val index_th1 = index_of_literal (s_not i_atm) prems_th1 handle Empty => raise Fail "Failed to find literal in th1" - val _ = trace_msg ctxt (fn () => " index_th1: " ^ Int.toString index_th1) + val _ = trace_msg ctxt (fn () => " index_th1: " ^ string_of_int index_th1) val index_th2 = index_of_literal i_atm prems_th2 handle Empty => raise Fail "Failed to find literal in th2" - val _ = trace_msg ctxt (fn () => " index_th2: " ^ Int.toString index_th2) + val _ = trace_msg ctxt (fn () => " index_th2: " ^ string_of_int index_th2) in resolve_inc_tyvars thy (select_literal thy index_th1 i_th1) index_th2 i_th2 @@ -458,10 +458,10 @@ val tm_p = List.nth(args,p') handle Subscript => error ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf: " ^ Int.toString p ^ " adj " ^ - Int.toString adjustment ^ " term " ^ + "equality_inf: " ^ string_of_int p ^ " adj " ^ + string_of_int adjustment ^ " term " ^ Syntax.string_of_term ctxt tm) - val _ = trace_msg ctxt (fn () => "path_finder: " ^ Int.toString p ^ + val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^ " " ^ Syntax.string_of_term ctxt tm_p) val (r,t) = path_finder_FO tm_p ps in @@ -473,7 +473,7 @@ | path_finder_HO tm ps = raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ "equality_inf, path_finder_HO: path = " ^ - space_implode " " (map Int.toString ps) ^ + space_implode " " (map string_of_int ps) ^ " isa-term: " ^ Syntax.string_of_term ctxt tm) fun path_finder_FT tm [] _ = (tm, Bound 0) | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) = @@ -485,7 +485,7 @@ | path_finder_FT tm ps t = raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ "equality_inf, path_finder_FT: path = " ^ - space_implode " " (map Int.toString ps) ^ + space_implode " " (map string_of_int ps) ^ " isa-term: " ^ Syntax.string_of_term ctxt tm ^ " fol-term: " ^ Metis_Term.toString t) fun path_finder FO tm ps _ = path_finder_FO tm ps diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jan 10 15:45:46 2011 +0100 @@ -150,7 +150,7 @@ val A_minus_space = Char.ord #"A" - Char.ord #" "; fun stringN_of_int 0 _ = "" - | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10); + | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ string_of_int (n mod 10); fun ascii_of_c c = if Char.isAlphaNum c then String.str c @@ -196,7 +196,7 @@ else error ("trim_type: Malformed type variable encountered: " ^ s); fun ascii_of_indexname (v,0) = ascii_of v - | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; + | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i; fun make_bound_var x = bound_var_prefix ^ ascii_of x fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v @@ -275,7 +275,7 @@ fun gen_TVars 0 = [] - | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1); + | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1); fun pack_sort(_,[]) = [] | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*) @@ -326,7 +326,7 @@ arity_clause seen n (tcons,ars) | arity_clause seen n (tcons, (ar as (class,_)) :: ars) = if member (op =) seen class then (*multiple arities for the same tycon, class pair*) - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: + make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) :: arity_clause seen (n+1) (tcons,ars) else make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: @@ -473,7 +473,7 @@ fun old_skolem_const_name i j num_T_args = old_skolem_const_prefix ^ Long_Name.separator ^ - (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args])) + (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args])) fun conceal_old_skolem_terms i old_skolems t = if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Jan 10 15:45:46 2011 +0100 @@ -143,7 +143,7 @@ val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm -fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j +fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j fun conceal_bounds Ts t = subst_bounds (map (Free o apfst concealed_bound_name) (0 upto length Ts - 1 ~~ Ts), t) @@ -247,7 +247,7 @@ | formula => SOME formula fun make_conjecture ctxt ts = let val last = length ts - 1 in - map2 (fn j => make_formula ctxt true true (Int.toString j) + map2 (fn j => make_formula ctxt true true (string_of_int j) (if j = last then Conjecture else Hypothesis)) (0 upto last) ts end diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jan 10 15:45:46 2011 +0100 @@ -95,7 +95,7 @@ fun make_name reserved multi j name = (name |> needs_quoting reserved name ? quote) ^ - (if multi then "(" ^ Int.toString j ^ ")" else "") + (if multi then "(" ^ string_of_int j ^ ")" else "") fun explode_interval _ (Facts.FromTo (i, j)) = i upto j | explode_interval max (Facts.From i) = i upto i + max - 1 @@ -482,8 +482,8 @@ chop max_imperfect imperfect |>> append perfect |>> chop remaining_max in trace_msg (fn () => - "Actually passed (" ^ Int.toString (length accepts) ^ " of " ^ - Int.toString (length candidates) ^ "): " ^ + "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^ + string_of_int (length candidates) ^ "): " ^ (accepts |> map (fn ((((name, _), _), _), weight) => name () ^ " [" ^ Real.toString weight ^ "]") |> commas)); @@ -612,7 +612,7 @@ accepts |> needs_ext is_built_in_const accepts ? add_facts @{thms ext}) |> tap (fn accepts => trace_msg (fn () => - "Total relevant: " ^ Int.toString (length accepts))) + "Total relevant: " ^ string_of_int (length accepts))) end @@ -886,7 +886,7 @@ |> rearrange_facts ctxt (respect_no_atp andalso not only) |> uniquify in - trace_msg (fn () => "Considering " ^ Int.toString (length facts) ^ + trace_msg (fn () => "Considering " ^ string_of_int (length facts) ^ " facts"); (if only orelse threshold1 < 0.0 then facts diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jan 10 15:45:46 2011 +0100 @@ -165,7 +165,7 @@ ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ (case length (filter (curry (op =) Chained o snd o fst) min_thms) of 0 => "" - | n => " (including " ^ Int.toString n ^ " chained)") ^ ".") + | n => " (including " ^ string_of_int n ^ " chained)") ^ ".") in (SOME min_thms, message) end | {outcome = SOME TimedOut, ...} => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Mon Jan 10 15:45:46 2011 +0100 @@ -309,7 +309,7 @@ then mk_functional_err "The function being declared appears with multiple types" else mk_functional_err - (Int.toString (length fs) ^ + (string_of_int (length fs) ^ " distinct function names being declared") in fun mk_functional thy clauses = @@ -340,7 +340,7 @@ of [] => () | L => mk_functional_err ("The following clauses are redundant (covered by preceding clauses): " ^ - commas (map (fn i => Int.toString (i + 1)) L)) + commas (map (fn i => string_of_int (i + 1)) L)) in {functional = Abs(Long_Name.base_name fname, ftype, abstract_over (atom, absfree(aname,atype, case_tm))), diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Tools/prop_logic.ML Mon Jan 10 15:45:46 2011 +0100 @@ -396,7 +396,7 @@ fun term_of_prop_formula True = HOLogic.true_const | term_of_prop_formula False = HOLogic.false_const - | term_of_prop_formula (BoolVar i) = Free ("v" ^ Int.toString i, HOLogic.boolT) + | term_of_prop_formula (BoolVar i) = Free ("v" ^ string_of_int i, HOLogic.boolT) | term_of_prop_formula (Not fm) = HOLogic.mk_not (term_of_prop_formula fm) | term_of_prop_formula (Or (fm1, fm2)) = HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2) diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Tools/sat_funcs.ML Mon Jan 10 15:45:46 2011 +0100 @@ -346,9 +346,9 @@ (if !trace_sat then tracing ("Proof trace from SAT solver:\n" ^ "clauses: " ^ ML_Syntax.print_list - (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) + (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int)) (Inttab.dest clause_table) ^ "\n" ^ - "empty clause: " ^ Int.toString empty_id) + "empty clause: " ^ string_of_int empty_id) else (); if !quick_and_dirty then make_quick_and_dirty_thm () diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/HOL/Tools/sat_solver.ML Mon Jan 10 15:45:46 2011 +0100 @@ -657,7 +657,7 @@ fun sat_to_proof id = ( case Inttab.lookup (!clause_id_map) id of SOME id' => id' - | NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.") + | NONE => raise INVALID_PROOF ("Clause ID " ^ string_of_int id ^ " used, but not defined.") ) val next_id = Unsynchronized.ref (number_of_clauses - 1) (* string list -> unit *) diff -r 0f1e411a1448 -r a2ad5b824051 src/Provers/blast.ML --- a/src/Provers/blast.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Provers/blast.ML Mon Jan 10 15:45:46 2011 +0100 @@ -651,7 +651,7 @@ fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = (fullTrace := brs0 :: !fullTrace; List.app (fn _ => Output.tracing "+") brs; - Output.tracing (" [" ^ Int.toString lim ^ "] "); + Output.tracing (" [" ^ string_of_int lim ^ "] "); printPairs pairs; writeln"") in if !trace then printBrs (map normBr brs) else () @@ -665,7 +665,7 @@ (case !ntrail-ntrl of 0 => () | 1 => Output.tracing "\t1 variable UPDATED:" - | n => Output.tracing ("\t" ^ Int.toString n ^ " variables UPDATED:"); + | n => Output.tracing ("\t" ^ string_of_int n ^ " variables UPDATED:"); (*display the instantiations themselves, though no variable names*) List.app (fn v => Output.tracing (" " ^ string_of thy 4 (the (!v)))) (List.take(!trail, !ntrail-ntrl)); @@ -678,7 +678,7 @@ case length prems of 0 => Output.tracing "branch closed by rule" | 1 => Output.tracing "branch extended (1 new subgoal)" - | n => Output.tracing ("branch split: "^ Int.toString n ^ " new subgoals") + | n => Output.tracing ("branch split: "^ string_of_int n ^ " new subgoals") else (); @@ -844,7 +844,7 @@ let val ll = length last and lc = length choices in if !trace andalso ll (writeln ("PROOF FAILED for depth " ^ - Int.toString lim); + string_of_int lim); if !trace then error "************************\n" else (); backtrack choices) diff -r 0f1e411a1448 -r a2ad5b824051 src/Pure/ML/ml_syntax.ML --- a/src/Pure/ML/ml_syntax.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Pure/ML/ml_syntax.ML Mon Jan 10 15:45:46 2011 +0100 @@ -49,7 +49,7 @@ val atomic = enclose "(" ")"; -val print_int = Int.toString; +val print_int = string_of_int; fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")"; diff -r 0f1e411a1448 -r a2ad5b824051 src/Pure/ProofGeneral/pgip_output.ML --- a/src/Pure/ProofGeneral/pgip_output.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Pure/ProofGeneral/pgip_output.ML Mon Jan 10 15:45:46 2011 +0100 @@ -282,7 +282,7 @@ val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory val guiseproof = elto "guiseproof" (fn thm=>(attr "thmname" thm) @ - (opt_attr "proofpos" (Option.map Int.toString proofpos))) theorem + (opt_attr "proofpos" (Option.map string_of_int proofpos))) theorem in XML.Elem (("informguise", []), guisefile @ guisetheory @ guiseproof) end diff -r 0f1e411a1448 -r a2ad5b824051 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jan 10 15:45:46 2011 +0100 @@ -498,7 +498,7 @@ let val times = #times vs in - isarcmd ("undos_proof " ^ Int.toString times) + isarcmd ("undos_proof " ^ string_of_int times) end fun redostep _ = raise Fail "redo unavailable" @@ -726,7 +726,7 @@ let val width = #width vs in - isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *) + isarcmd ("pretty_setmargin " ^ string_of_int width) (* FIXME: conversion back/forth! *) end fun viewdoc (Viewdoc vs) = diff -r 0f1e411a1448 -r a2ad5b824051 src/Tools/WWW_Find/find_theorems.ML --- a/src/Tools/WWW_Find/find_theorems.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Tools/WWW_Find/find_theorems.ML Mon Jan 10 15:45:46 2011 +0100 @@ -30,7 +30,7 @@ label (noid, { for = "limit" }, "Max. results:"), input (id "limit", { name = "limit", - itype = TextInput { value = SOME (Int.toString limit), + itype = TextInput { value = SOME (string_of_int limit), maxlength = NONE }}) ]; @@ -116,20 +116,20 @@ val args = (case othmslen of NONE => args - | SOME l => Symtab.update ("limit", Int.toString l) args) + | SOME l => Symtab.update ("limit", string_of_int l) args) val qargs = HttpUtil.make_query_string args; val num_found_text = (case othmslen of - NONE => text (Int.toString thmslen) + NONE => text (string_of_int thmslen) | SOME l => a { href = find_theorems_url ^ (if qargs = "" then "" else "?" ^ qargs), - text = Int.toString l }) + text = string_of_int l }) val found = [text "found ", num_found_text, text " theorems"] : tag list; val displayed = if is_some othmslen - then " (" ^ Int.toString thmslen ^ " displayed)" + then " (" ^ string_of_int thmslen ^ " displayed)" else ""; fun show_search c = tr [ td' noid [show_criterion c] ]; in @@ -147,7 +147,7 @@ Output.output o Pretty.string_of_margin 100 o Display.pretty_thm (Config.put show_question_marks false ctxt); in - tag' "tr" (class ("row" ^ Int.toString (n mod 2))) + tag' "tr" (class ("row" ^ string_of_int (n mod 2))) [ tag' "td" (class "name") [span' (sorry_class thm) diff -r 0f1e411a1448 -r a2ad5b824051 src/Tools/WWW_Find/html_unicode.ML --- a/src/Tools/WWW_Find/html_unicode.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Tools/WWW_Find/html_unicode.ML Mon Jan 10 15:45:46 2011 +0100 @@ -45,7 +45,7 @@ if Symbol.is_raw s then (1, Symbol.decode_raw s) else (case UnicodeSymbols.symbol_to_unicode s of - SOME x => (sym_width s, "&#" ^ Int.toString x ^ ";") (* numeric entities *) + SOME x => (sym_width s, "&#" ^ string_of_int x ^ ";") (* numeric entities *) (* SOME x => (sym_width s, UnicodeSymbols.utf8 [x]) (* utf-8 *) *) | NONE => (size s, XML.text s)); diff -r 0f1e411a1448 -r a2ad5b824051 src/Tools/WWW_Find/http_util.ML --- a/src/Tools/WWW_Find/http_util.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Tools/WWW_Find/http_util.ML Mon Jan 10 15:45:46 2011 +0100 @@ -21,7 +21,7 @@ fun reply_header (status, content_type, extra_fields) = let - val code = (Int.toString o HttpStatus.to_status_code) status; + val code = (string_of_int o HttpStatus.to_status_code) status; val reason = HttpStatus.to_reason status; val show_content_type = pair "Content-Type" o Mime.show_type; in diff -r 0f1e411a1448 -r a2ad5b824051 src/Tools/WWW_Find/scgi_req.ML --- a/src/Tools/WWW_Find/scgi_req.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Tools/WWW_Find/scgi_req.ML Mon Jan 10 15:45:46 2011 +0100 @@ -80,7 +80,7 @@ val nulls = ~1 :: (Word8Vector.foldri find_nulls [] vec); fun pr NONE = "NONE" - | pr (SOME i) = "SOME " ^ Int.toString i; + | pr (SOME i) = "SOME " ^ string_of_int i; fun hd_diff (i1::i2::_) = SOME (i2 - i1 - 1) | hd_diff _ = NONE; diff -r 0f1e411a1448 -r a2ad5b824051 src/Tools/WWW_Find/scgi_server.ML --- a/src/Tools/WWW_Find/scgi_server.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Tools/WWW_Find/scgi_server.ML Mon Jan 10 15:45:46 2011 +0100 @@ -115,8 +115,8 @@ server server_prefix port handle OS.SysErr ("bind failed", _) => (warning ("Could not acquire port " - ^ Int.toString port ^ ". Trying again in " - ^ Int.toString delay ^ " seconds..."); + ^ string_of_int port ^ ". Trying again in " + ^ string_of_int delay ^ " seconds..."); OS.Process.sleep (Time.fromSeconds delay); server' (countdown - 1) server_prefix port); end; diff -r 0f1e411a1448 -r a2ad5b824051 src/Tools/WWW_Find/socket_util.ML --- a/src/Tools/WWW_Find/socket_util.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Tools/WWW_Find/socket_util.ML Mon Jan 10 15:45:46 2011 +0100 @@ -41,7 +41,7 @@ val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock); val sock_name = - String.concat [ NetHostDB.toString haddr, ":", Int.toString port ]; + String.concat [ NetHostDB.toString haddr, ":", string_of_int port ]; val rd = BinPrimIO.RD { diff -r 0f1e411a1448 -r a2ad5b824051 src/Tools/WWW_Find/xhtml.ML --- a/src/Tools/WWW_Find/xhtml.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Tools/WWW_Find/xhtml.ML Mon Jan 10 15:45:46 2011 +0100 @@ -270,7 +270,7 @@ fun ostr_att (nm, NONE) = [] | ostr_att (nm, SOME s) = [(nm, s)]; -val oint_att = ostr_att o apsnd (Option.map Int.toString); +val oint_att = ostr_att o apsnd (Option.map string_of_int); val table = tag' "table"; val thead = tag' "thead"; @@ -291,7 +291,7 @@ fun p' (common_atts, tags) = Tag ("p", from_common common_atts, tags); fun h (common_atts, i, text) = - Tag ("h" ^ Int.toString i, from_common common_atts, [Text text]); + Tag ("h" ^ string_of_int i, from_common common_atts, [Text text]); fun strong t = Tag ("strong", [], [Text t]); fun em t = Tag ("em", [], [Text t]); @@ -341,7 +341,7 @@ @ oint_att ("maxlength", maxlength) | input_atts (Password NONE) = [("type", "password")] | input_atts (Password (SOME i)) = - [("type", "password"), ("maxlength", Int.toString i)] + [("type", "password"), ("maxlength", string_of_int i)] | input_atts (Checkbox checked) = ("type", "checkbox") :: from_checked checked | input_atts (Radio checked) = ("type", "radio") :: from_checked checked