# HG changeset patch
# User wenzelm
# Date 1473280110 -7200
# Node ID 52235c27538caf83bde1d31340dd8bddba98f136
# Parent  5f8643e8ced5a968819eb58113eb32029e222c0c
unfold_abs_def is enabled by default;

diff -r 5f8643e8ced5 -r 52235c27538c NEWS
--- a/NEWS	Tue Sep 06 21:36:48 2016 +0200
+++ b/NEWS	Wed Sep 07 22:28:30 2016 +0200
@@ -66,7 +66,15 @@
 is relevant to avoid confusion of Pure.simp vs. HOL.simp.
 
 * Commands 'prf' and 'full_prf' are somewhat more informative (again):
-proof terms are reconstructed and cleaned from administrative thm nodes.
+proof terms are reconstructed and cleaned from administrative thm
+nodes.
+
+* The command 'unfolding' and proof method "unfold" include a second
+stage where given equations are passed through the attribute "abs_def"
+before rewriting. This ensures that definitions are fully expanded,
+regardless of the actual parameters that are provided. Rare
+INCOMPATIBILITY in some corner cases: use proof method (simp only:)
+instead, or declare [[unfold_abs_def = false]] in the proof context.
 
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
diff -r 5f8643e8ced5 -r 52235c27538c src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Tue Sep 06 21:36:48 2016 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed Sep 07 22:28:30 2016 +0200
@@ -84,6 +84,11 @@
   fold back) the given definitions throughout all goals; any chained facts
   provided are inserted into the goal and subject to rewriting as well.
 
+  Unfolding works in two stages: first, the given equations are used directly
+  for rewriting; second, the equations are passed through the attribute
+  @{attribute_ref abs_def} before rewriting --- to ensure that definitions are
+  fully expanded, regardless of the actual parameters that are provided.
+
   \<^descr> @{method insert}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> inserts theorems as facts into all goals of
   the proof state. Note that current facts indicated for forward chaining are
   ignored.
@@ -155,8 +160,8 @@
   expand and fold back again the given definitions throughout a rule.
 
   \<^descr> @{attribute abs_def} turns an equation of the form @{prop "f x y \<equiv> t"}
-  into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method simp} or @{method
-  unfold} steps always expand it. This also works for object-logic equality.
+  into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method simp} steps always
+  expand it. This also works for object-logic equality.
 
   \<^descr> @{attribute rotated}~\<open>n\<close> rotate the premises of a theorem by \<open>n\<close> (default
   1).
diff -r 5f8643e8ced5 -r 52235c27538c src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Tue Sep 06 21:36:48 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Sep 07 22:28:30 2016 +0200
@@ -332,8 +332,8 @@
   "proof"}).
 
   \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally similar to @{command
-  "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the
-  goal state and facts.
+  "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the goal
+  state and facts. See also the proof method @{method_ref unfold}.
 
   \<^descr> \<^theory_text>\<open>(use b\<^sub>1 \<dots> b\<^sub>n in method)\<close> uses the facts in the given method
   expression. The facts provided by the proof state (via @{command "using"}
diff -r 5f8643e8ced5 -r 52235c27538c src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Sep 06 21:36:48 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Sep 07 22:28:30 2016 +0200
@@ -207,7 +207,7 @@
 
 (* unfold object-level rules *)
 
-val unfold_abs_def_raw = Config.declare ("unfold_abs_def", @{here}) (K (Config.Bool false));
+val unfold_abs_def_raw = Config.declare ("unfold_abs_def", @{here}) (K (Config.Bool true));
 val unfold_abs_def = Config.bool unfold_abs_def_raw;
 
 local