# HG changeset patch
# User blanchet
# Date 1311863568 -7200
# Node ID ae53f1304ad5ab4bfa7d0317ed19f4c35acde8a6
# Parent  2b75760fa75ea77d2f413b4b81a7b663e7f6a859
put parentheses around non-trivial metis call

diff -r 2b75760fa75e -r ae53f1304ad5 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jul 28 16:32:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jul 28 16:32:48 2011 +0200
@@ -206,7 +206,8 @@
   | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
   | apply_on_subgoal settings i n =
     "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
-fun command_call name [] = name
+fun command_call name [] =
+    name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
 fun try_command_line banner time command =
   banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "."