# HG changeset patch # User blanchet # Date 1409237907 -7200 # Node ID d44c9dc4bf3095dc503f4352a956306d2b50e8ad # Parent f050a297c9c30e599e2d5a9edc1a2b281f5e7400 took out one more occurrence of 'PolyML.makestring' diff -r f050a297c9c3 -r d44c9dc4bf30 src/HOL/Tools/SMT/verit_proof.ML --- a/src/HOL/Tools/SMT/verit_proof.ML Thu Aug 28 16:58:27 2014 +0200 +++ b/src/HOL/Tools/SMT/verit_proof.ML Thu Aug 28 16:58:27 2014 +0200 @@ -163,7 +163,7 @@ let fun rotate_pair (a, (b, c)) = ((a, b), c) fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l) - | get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t) + | get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t) fun parse_rule (SMTLIB.Sym rule :: l) = (rule, l) fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) = (SOME (map (fn (SMTLIB.Sym id) => id) source), l)