diff -r 455ca98d9de3 -r 882abe912da9 src/HOL/Tools/value_command.ML
--- a/src/HOL/Tools/value_command.ML	Sat Aug 05 22:12:41 2017 +0200
+++ b/src/HOL/Tools/value_command.ML	Sun Aug 06 15:02:54 2017 +0200
@@ -17,9 +17,7 @@
 
 fun default_value ctxt t =
   if null (Term.add_frees t [])
-  then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
-    SOME t' => t'
-  | NONE => Nbe.dynamic_value ctxt t
+  then Code_Evaluation.dynamic_value_strict ctxt t
   else Nbe.dynamic_value ctxt t;
 
 structure Evaluator = Theory_Data