# HG changeset patch
# User wenzelm
# Date 1697969903 -7200
# Node ID 1829ba610c36f430b2312fdaff2a63d4efc51d3d
# Parent  d769a183d51dec02ff1d06b7f0d322ba04d6dccd
proper morphism;

diff -r d769a183d51d -r 1829ba610c36 NEWS
--- a/NEWS	Sat Oct 21 21:19:02 2023 +0200
+++ b/NEWS	Sun Oct 22 12:18:23 2023 +0200
@@ -50,7 +50,8 @@
   begin
 
   ML \<open>
-    \<^simproc_setup>\<open>foo (x) = \<open>fn _ => fn _ => fn _ => SOME @{thm eq}\<close>
+    \<^simproc_setup>\<open>foo (x) =
+      \<open>fn phi => fn _ => fn _ => SOME (Morphism.thm phi @{thm eq})\<close>
       identifier test_axioms\<close>
   \<close>