diff -r 455ca98d9de3 -r 882abe912da9 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sat Aug 05 22:12:41 2017 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Aug 06 15:02:54 2017 +0200
@@ -38,7 +38,7 @@
 adhoc_overloading
   vars term_vars
 
-value "vars (Fun ''f'' [Var 0, Var 1])"
+value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
 
 fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
   "rule_vars (l, r) = vars l \<union> vars r"
@@ -46,7 +46,7 @@
 adhoc_overloading
   vars rule_vars
 
-value "vars (Var 1, Var 0)"
+value [nbe] "vars (Var 1, Var 0)"
 
 definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
   "trs_vars R = \<Union>(rule_vars ` R)"
@@ -54,7 +54,7 @@
 adhoc_overloading
   vars trs_vars
 
-value "vars {(Var 1, Var 0)}"
+value [nbe] "vars {(Var 1, Var 0)}"
 
 text \<open>Sometimes it is necessary to add explicit type constraints
 before a variant can be determined.\<close>