src/HOL/Tools/SMT/smt_solver.ML

         Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
   end
 
 in
 
-fun invoke memoize_fun_call name command options smt_options ithms ctxt =
-  let
-    val options = options @ SMT_Config.solver_options_of ctxt
+fun invoke memoize_fun_call name command cmd_options smt_options ithms ctxt =
+  let
+    val options = cmd_options @ SMT_Config.solver_options_of ctxt
     val comments = [implode_space options]
 
-    val (str, replay_data as {context = ctxt', ...}) =
+    val (input, replay_data as {context = ctxt', ...}) =
       ithms
       |> tap (trace_assms ctxt)
       |> SMT_Translate.translate ctxt name smt_options comments
       ||> tap trace_replay_data
 
     val cmd = Bash.script (Bash.strings (command () @ options))
     val run_cmd = run_solver ctxt' name cmd
 
     val output_lines =
       (case memoize_fun_call of
-        NONE => run_cmd str
-      | SOME memoize => split_lines (memoize (cat_lines o run_cmd) str))
+        NONE => run_cmd input
+      | SOME memoize => split_lines (memoize (cat_lines o run_cmd) input))
   in (output_lines, replay_data) end
 
 end