--- 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) =>
--- 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')
--- 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
--- 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",
"",
--- 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])));
--- 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
--- 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)
--- 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
--- 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))
--- 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)
--- 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
--- 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) =
--- 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' =>
--- 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
--- 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
--- 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
--- 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
--- 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\" \
--- 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))),
--- 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)
--- 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 ()
--- 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 *)
--- 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<lc then
- (writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels");
+ (writeln("Pruning " ^ string_of_int(lc-ll) ^ " levels");
last)
else last
end
@@ -865,7 +865,7 @@
fun backtrack (choices as (ntrl, nbrs, exn)::_) =
(if !trace then (writeln ("Backtracking; now there are " ^
- Int.toString nbrs ^ " branches"))
+ string_of_int nbrs ^ " branches"))
else ();
raise exn)
| backtrack _ = raise PROVE;
@@ -915,9 +915,9 @@
fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
if b then
writeln (#message (end_timing start) ^ " for search. Closed: "
- ^ Int.toString (!nclosed) ^
- " tried: " ^ Int.toString (!ntried) ^
- " tactics: " ^ Int.toString (length tacs))
+ ^ string_of_int (!nclosed) ^
+ " tried: " ^ string_of_int (!ntried) ^
+ " tactics: " ^ string_of_int (length tacs))
else ();
@@ -1260,7 +1260,7 @@
in
case Seq.pull(EVERY' (rev tacs) i st) of
NONE => (writeln ("PROOF FAILED for depth " ^
- Int.toString lim);
+ string_of_int lim);
if !trace then error "************************\n"
else ();
backtrack choices)
--- 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 ^ ")";
--- 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
--- 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) =
--- 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)
--- 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));
--- 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
--- 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;
--- 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;
--- 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 {
--- 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