--- 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);