src/HOL/Tools/res_atp.ML

   else error ("No such directory: " ^ !destdir);
 
 fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
 
 
-(**** for Isabelle/ML interface  ****)
-
-(*Remove unwanted characters such as ? and newline from the textural 
-  representation of a theorem (surely they don't need to be produced in 
-  the first place?) *)
-
-fun is_proof_char ch = (#" " <= ch andalso ch <= #"~" andalso ch <> #"?");
-
-val proofstring =
-    String.translate (fn c => if is_proof_char c then str c else "");
-
-
 (**** For running in Isar ****)
 
 (* same function as that in res_axioms.ML *)
 fun repeat_RS thm1 thm2 =
     let val thm1' =  thm1 RS thm2 handle THM _ => thm1

 fun watcher_call_provers sign sg_terms (childin, childout,pid) =
   let
     fun make_atp_list [] n = []
       | make_atp_list (sg_term::xs) n =
           let
-            val goalstring = proofstring (Sign.string_of_term sign sg_term)
+            val goalstring = Sign.string_of_term sign sg_term
             val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
             val probfile = prob_pathname n
             val time = Int.toString (!time_limit)
             val _ = debug ("problem file in watcher_call_provers is " ^ probfile)
           in

     if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
     else isar_atp_writeonly (ctxt, goal)
   end);
 
 val call_atpP =
-  OuterSyntax.improper_command 
+  OuterSyntax.command 
     "ProofGeneral.call_atp" 
     "call automatic theorem provers" 
     OuterKeyword.diag
     (Scan.succeed (Toplevel.no_timing o invoke_atp));