# HG changeset patch
# User blanchet
# Date 1409121672 -7200
# Node ID a90847f03ec8aaae328f52877d6e761d5fcf8fce
# Parent  ffa9e39763e3cf971f3943b6b2438d0c336b46f6
avoid 'PolyML.makestring'

diff -r ffa9e39763e3 -r a90847f03ec8 src/HOL/Tools/ATP/atp_satallax.ML
--- a/src/HOL/Tools/ATP/atp_satallax.ML	Mon Aug 25 14:24:05 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML	Wed Aug 27 08:41:12 2014 +0200
@@ -99,7 +99,7 @@
           if state = 1 orelse state = 0 then
             sep_dep l used_assumptions (x :: new_goals) generated_assumptions 1
           else
-            raise Fail ("incorrect Satallax proof" ^ PolyML.makestring l)
+            raise Fail ("incorrect Satallax proof: " ^ @{make_string} l)
   in
     sep_dep dependencies [] [] [] 0
   end
@@ -154,7 +154,7 @@
 
 fun find_proof_step ((x as Satallax_Step {id, ...}) :: l) h =
     if h = id then x else find_proof_step l h
-  | find_proof_step [] h = raise Fail ("not_found: " ^ PolyML.makestring h ^ "(probably a parsing \
+  | find_proof_step [] h = raise Fail ("not_found: " ^ @{make_string} h ^ " (probably a parsing \
     \error)")
 
 fun remove_not_not (x as ATerm ((op1, _), [ATerm ((op2, _), [th])])) =