# HG changeset patch # User wenzelm # Date 1738072388 -3600 # Node ID 7301923ad1e93cf126dcaafeef876f1f0ffe3637 # Parent 04c704a6b193b7013a8ed79d0010587349123c21 tuned; diff -r 04c704a6b193 -r 7301923ad1e9 src/Pure/Tools/adhoc_overloading.ML --- a/src/Pure/Tools/adhoc_overloading.ML Tue Jan 28 13:42:40 2025 +0100 +++ b/src/Pure/Tools/adhoc_overloading.ML Tue Jan 28 14:53:08 2025 +0100 @@ -112,7 +112,7 @@ fun generic_variant add oconst t context = let val _ = if has_variants context oconst then () else err_not_overloaded oconst; - val T = t |> fastype_of; + val T = fastype_of t; val t' = Term.map_types (K dummyT) t; in if add then @@ -187,20 +187,18 @@ Pattern.rewrite_term_yoyo thy [] [proc] end; -fun add_consts_overloaded ctxt = +fun overloaded_term_consts ctxt = let val context = Context.Proof ctxt; val overloaded = has_variants context; - in - if no_variants context then K I - else fold_aterms (fn Const (c, T) => if overloaded c then insert (op =) (c, T) else I | _ => I) - end; + val add = fn Const (c, T) => if overloaded c then insert (op =) (c, T) else I | _ => I; + in fn t => if no_variants context then [] else fold_aterms add t [] end; in fun check ctxt = if no_variants (Context.Proof ctxt) then I - else map (fn t => Term.map_aterms (insert_variants_same ctxt t) t); + else map (fn t => t |> Term.map_aterms (insert_variants_same ctxt t)); fun uncheck ctxt ts = if Config.get ctxt show_variants orelse exists (not o can Term.type_of) ts then ts @@ -209,7 +207,7 @@ fun reject_unresolved ctxt = let fun check_unresolved t = - (case add_consts_overloaded ctxt t [] of + (case overloaded_term_consts ctxt t of [] => t | const :: _ => err_unresolved_overloading ctxt const t (the_candidates ctxt const)); in map check_unresolved end;