src/Pure/System/isabelle_process.scala

     if (proc == null) error("Cannot output to Isabelle: no process")
     if (closing) error("Cannot output to Isabelle: already closing")
     command_input ! Input(" \\<^sync>\n; " + text + " \\<^sync>;\n")
   }
 
-  def command(text: String) = input("Isabelle.command " + Isabelle_Syntax.encode_string(text))
-
-  def command(props: List[(String, String)], text: String) =
-    input("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
-      Isabelle_Syntax.encode_string(text))
-
-  def ML_val(text: String) = input("ML_val " + Isabelle_Syntax.encode_string(text))
-  def ML_command(text: String) = input("ML_command " + Isabelle_Syntax.encode_string(text))
-
   def close() = synchronized {    // FIXME avoid synchronized
     command_input ! Close
     closing = true
   }