| changeset 69593 | 3dda49e08b9d |
| parent 67149 | e61557884799 |
| child 74508 | 3315c551fe6e |
--- a/src/Tools/solve_direct.ML Fri Jan 04 21:49:06 2019 +0100 +++ b/src/Tools/solve_direct.ML Fri Jan 04 23:22:53 2019 +0100 @@ -100,6 +100,6 @@ fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try) val _ = - Try.tool_setup (solve_directN, (10, @{system_option auto_solve_direct}, try_solve_direct)); + Try.tool_setup (solve_directN, (10, \<^system_option>\<open>auto_solve_direct\<close>, try_solve_direct)); end;