Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Thu, 18 May 2023 23:20:41 +0200
changeset 78073 b8dfaba8394f
parent 78072 001739cb8d08
child 78074 073826f50e14
tuned;
src/Pure/Isar/expression.ML file | annotate | diff | comparison | revisions 
--- 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' =
isabelle