took out one more occurrence of 'PolyML.makestring'
authorblanchet
Thu Aug 28 16:58:27 2014 +0200 (2014-08-28)
changeset 58078d44c9dc4bf30
parent 58077 f050a297c9c3
child 58079 df0d6ce8fb66
took out one more occurrence of 'PolyML.makestring'
src/HOL/Tools/SMT/verit_proof.ML
     1.1 --- a/src/HOL/Tools/SMT/verit_proof.ML	Thu Aug 28 16:58:27 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/verit_proof.ML	Thu Aug 28 16:58:27 2014 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4    let
     1.5      fun rotate_pair (a, (b, c)) = ((a, b), c)
     1.6      fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l)
     1.7 -      | get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t)
     1.8 +      | get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t)
     1.9      fun parse_rule (SMTLIB.Sym rule :: l) = (rule, l)
    1.10      fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) =
    1.11          (SOME (map (fn (SMTLIB.Sym id) => id) source), l)