# HG changeset patch
# User wenzelm
# Date 1684444841 -7200
# Node ID b8dfaba8394f0536f97deddb69ac31cb10fad6a4
# Parent  001739cb8d087d9a2ad6a76ff05062a54a482e22
tuned;

diff -r 001739cb8d08 -r b8dfaba8394f src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu May 18 17:21:29 2023 +0200
+++ b/src/Pure/Isar/expression.ML	Thu May 18 23:20:41 2023 +0200
@@ -794,7 +794,7 @@
 fun defines_to_notes ctxt (Defines defs) =
       Notes ("", map (fn (a, (def, _)) =>
         (a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)],
-          [(Attrib.internal o K) Locale.witness_add])])) defs)
+          [Attrib.internal (K Locale.witness_add)])])) defs)
   | defines_to_notes _ e = e;
 
 val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
@@ -846,7 +846,7 @@
       if is_some asm then
         [("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []),
           [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))],
-            [(Attrib.internal o K) Locale.witness_add])])])]
+            [Attrib.internal (K Locale.witness_add)])])])]
       else [];
 
     val notes' =