Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/value_command.ML
changeset 66345 882abe912da9
parent 63806 c54a53ef1873
child 67149 e61557884799 
--- 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
isabelle