diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/ex/Adhoc_Overloading_Examples.thy --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Sun Jan 27 17:30:09 2019 +0100 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Mon Jan 28 10:27:47 2019 +0100 @@ -26,7 +26,7 @@ text \The set of variables of a term might be computed as follows.\ fun term_vars :: "('a, 'b) term \ 'b set" where "term_vars (Var x) = {x}" | - "term_vars (Fun f ts) = \set (map term_vars ts)" + "term_vars (Fun f ts) = \(set (map term_vars ts))" text \However, also for \emph{rules} (i.e., pairs of terms) and term rewrite systems (i.e., sets of rules), the set of variables makes