# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1503405266 -7200
# Node ID ddb31006e3150fbbc4a11eb9893f06210c36d8da
# Parent  e904aa5220681025c7c5aa43f726f6f885c37cfa
tuned

diff -r e904aa522068 -r ddb31006e315 src/HOL/Library/Pattern_Aliases.thy
--- a/src/HOL/Library/Pattern_Aliases.thy	Tue Aug 22 11:56:17 2017 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy	Tue Aug 22 14:34:26 2017 +0200
@@ -27,7 +27,13 @@
     appear in the output.
   \<^item> To obtain reasonable induction principles in function definitions, the bundle also declares
     a custom congruence rule for @{const Let} that only affects @{command fun}. This congruence
-    rule might lead to an explosion in term size (although that is rare)!
+    rule might lead to an explosion in term size (although that is rare)! In some circumstances
+    (using \<open>let\<close> to destructure tuples), the internal construction of functions stumbles over this
+    rule and prints an error. To mitigate this, either
+    \<^item> activate the bundle locally (@{theory_text \<open>context includes ... begin\<close>}) or
+    \<^item> rewrite the \<open>let\<close>-expression to use \<open>case\<close>: @{term \<open>let (a, b) = x in (b, a)\<close>} becomes
+      @{term \<open>case x of (a, b) \<Rightarrow> (b, a)\<close>}.
+  \<^item> The bundle also adds the @{thm Let_def} rule to the simpset.
 \<close>
 
 
@@ -160,6 +166,7 @@
   declaration \<open>K (Syntax_Phases.term_uncheck 98 "pattern_syntax" (map o uncheck_pattern_syntax))\<close>
 
   declare let_cong_unfolding [fundef_cong]
+  declare Let_def [simp]
 
 end