1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jul 28 16:32:39 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jul 28 16:32:48 2011 +0200
     1.3 @@ -206,7 +206,8 @@
     1.4    | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
     1.5    | apply_on_subgoal settings i n =
     1.6      "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
     1.7 -fun command_call name [] = name
     1.8 +fun command_call name [] =
     1.9 +    name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
    1.10    | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
    1.11  fun try_command_line banner time command =
    1.12    banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "."