--- a/src/HOL/Tools/ATP/atp_satallax.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/ATP/atp_satallax.ML Fri Jan 04 23:22:53 2019 +0100
@@ -101,7 +101,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: " ^ @{make_string} l)
+ raise Fail ("incorrect Satallax proof: " ^ \<^make_string> l)
in
sep_dep dependencies [] [] [] 0
end
@@ -156,7 +156,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: " ^ @{make_string} 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])])) =