diff -r 310114bec0d7 -r ceb324e34c14 src/HOL/Tools/value_command.ML
--- a/src/HOL/Tools/value_command.ML	Thu Jan 25 11:29:52 2018 +0100
+++ b/src/HOL/Tools/value_command.ML	Thu Jan 25 14:13:55 2018 +0100
@@ -76,7 +76,7 @@
   (Thy_Output.antiquotation_pretty_source \<^binding>\<open>value\<close>
     (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
     (fn ctxt => fn ((name, style), t) =>
-      [Thy_Output.pretty_term ctxt (style (value_select name ctxt t))])
+      Thy_Output.pretty_term ctxt (style (value_select name ctxt t)))
   #> add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
   #> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
   #> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);