--- a/src/Pure/Pure.thy Sun Jan 26 22:45:57 2025 +0100
+++ b/src/Pure/Pure.thy Mon Jan 27 12:13:37 2025 +0100
@@ -96,6 +96,7 @@
and "realizers" :: thy_decl
and "realizability" :: thy_decl
and "extract_type" "extract" :: thy_decl
+ and "adhoc_overloading" "no_adhoc_overloading" :: thy_decl
and "find_theorems" "find_consts" :: diag
and "named_theorems" :: thy_decl
abbrevs "\\tag" = "\<^marker>\<open>tag \<close>"
@@ -1416,6 +1417,27 @@
in end\<close>
+subsubsection \<open>Adhoc overloading\<close>
+
+ML \<open>
+local
+
+val _ =
+ Outer_Syntax.local_theory \<^command_keyword>\<open>adhoc_overloading\<close>
+ "add adhoc overloading for constants / fixed variables"
+ (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term)
+ >> Adhoc_Overloading.adhoc_overloading_cmd true);
+
+val _ =
+ Outer_Syntax.local_theory \<^command_keyword>\<open>no_adhoc_overloading\<close>
+ "delete adhoc overloading for constants / fixed variables"
+ (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term)
+ >> Adhoc_Overloading.adhoc_overloading_cmd false);
+
+in end
+\<close>
+
+
subsubsection \<open>Find consts and theorems\<close>
ML \<open>