# HG changeset patch
# User wenzelm
# Date 1632909309 -7200
# Node ID b9331caf92c3346d42802028c70aa155cdebca9b
# Parent  930047942f468df22ed0c1016ae21d440d9000ec
clarified examples;

diff -r 930047942f46 -r b9331caf92c3 NEWS
--- a/NEWS	Wed Sep 29 06:56:39 2021 +0000
+++ b/NEWS	Wed Sep 29 11:55:09 2021 +0200
@@ -298,11 +298,11 @@
 
   val natT = \<^Type>\<open>nat\<close>;
   fun mk_funT (A, B) = \<^Type>\<open>fun A B\<close>;
-  val dest_funT = fn \<^Type>\<open>fun A B\<close> => (A, B);
+  val dest_funT = \<^Type_fn>\<open>fun A B => \<open>(A, B)\<close>\<close>;
   fun mk_conj (A, B) = \<^Const>\<open>conj for A B\<close>;
-  val dest_conj = fn \<^Const_>\<open>conj for A B\<close> => (A, B);
+  val dest_conj = \<^Const_fn>\<open>conj for A B => \<open>(A, B)\<close>\<close>;
   fun mk_eq T (t, u) = \<^Const>\<open>HOL.eq T for t u\<close>;
-  val dest_eq = fn \<^Const_>\<open>HOL.eq T for t u\<close> => (T, (t, u));
+  val dest_eq = \<^Const_fn>\<open>HOL.eq T for t u => \<open>(T, (t, u))\<close>\<close>;
 
 * The "build" combinators of various data structures help to build
 content from bottom-up, by applying an "add" function the "empty" value.