# HG changeset patch
# User wenzelm
# Date 1461850972 -7200
# Node ID 8b9401bfd9fd77eb38aee99491db01afe61d0156
# Parent  0a8a75e400daed46277bc7284faad9a896fb6114
unfold is subject to unfold_abs_def (still inactive);
tuned signature;

diff -r 0a8a75e400da -r 8b9401bfd9fd src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Apr 28 11:47:01 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Apr 28 15:42:52 2016 +0200
@@ -471,7 +471,7 @@
 
 fun mk_sel_transfer_tac ctxt n sel_defs case_transfer =
   TRYALL Goal.conjunction_tac THEN
-  unfold_thms_tac ctxt (map (Drule.abs_def o Local_Defs.meta_rewrite_rule ctxt) sel_defs) THEN
+  unfold_thms_tac ctxt (map (Local_Defs.abs_def_rule ctxt) sel_defs) THEN
   ALLGOALS (rtac ctxt (mk_rel_funDN n case_transfer) THEN_ALL_NEW
     REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt rel_funI));
 
diff -r 0a8a75e400da -r 8b9401bfd9fd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Apr 28 11:47:01 2016 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Apr 28 15:42:52 2016 +0200
@@ -581,8 +581,7 @@
     (add_del Local_Defs.defn_add Local_Defs.defn_del)
     "declaration of definitional transformations" #>
   setup @{binding abs_def}
-    (Scan.succeed (Thm.rule_attribute [] (fn context =>
-      Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
+    (Scan.succeed (Thm.rule_attribute [] (Local_Defs.abs_def_rule o Context.proof_of)))
     "abstract over free variables of definitional theorem" #>
 
   register_config Goal.quick_and_dirty_raw #>
@@ -619,7 +618,8 @@
   register_config Raw_Simplifier.simp_depth_limit_raw #>
   register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
   register_config Raw_Simplifier.simp_debug_raw #>
-  register_config Raw_Simplifier.simp_trace_raw);
+  register_config Raw_Simplifier.simp_trace_raw #>
+  register_config Local_Defs.unfold_abs_def_raw);
 
 
 (* internal source *)
diff -r 0a8a75e400da -r 8b9401bfd9fd src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Thu Apr 28 11:47:01 2016 +0200
+++ b/src/Pure/Isar/interpretation.ML	Thu Apr 28 15:42:52 2016 +0200
@@ -116,8 +116,7 @@
 
 local
 
-fun meta_rewrite eqns ctxt =
-  (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
+fun meta_rewrite eqns ctxt = (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
 
 fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
   let
diff -r 0a8a75e400da -r 8b9401bfd9fd src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Apr 28 11:47:01 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Apr 28 15:42:52 2016 +0200
@@ -23,6 +23,9 @@
   val defn_del: attribute
   val meta_rewrite_conv: Proof.context -> conv
   val meta_rewrite_rule: Proof.context -> thm -> thm
+  val abs_def_rule: Proof.context -> thm -> thm
+  val unfold_abs_def_raw: Config.raw
+  val unfold_abs_def: bool Config.T
   val unfold: Proof.context -> thm list -> thm -> thm
   val unfold_goals: Proof.context -> thm list -> thm -> thm
   val unfold_tac: Proof.context -> thm list -> tactic
@@ -196,17 +199,31 @@
 
 val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv;
 
+fun abs_def_rule ctxt = meta_rewrite_rule ctxt #> Drule.abs_def;
+
 
 (* rewriting with object-level rules *)
 
+val unfold_abs_def_raw = Config.declare ("unfold_abs_def", @{here}) (K (Config.Bool false));
+val unfold_abs_def = Config.bool unfold_abs_def_raw;
+
+local
+
+fun meta_abs f ctxt =
+  f ctxt o map (meta_rewrite_rule ctxt #> Config.get ctxt unfold_abs_def ? Drule.abs_def);
+
 fun meta f ctxt = f ctxt o map (meta_rewrite_rule ctxt);
 
-val unfold       = meta Raw_Simplifier.rewrite_rule;
-val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule;
-val unfold_tac   = meta Raw_Simplifier.rewrite_goals_tac;
+in
+
+val unfold       = meta_abs Raw_Simplifier.rewrite_rule;
+val unfold_goals = meta_abs Raw_Simplifier.rewrite_goals_rule;
+val unfold_tac   = meta_abs Raw_Simplifier.rewrite_goals_tac;
 val fold         = meta Raw_Simplifier.fold_rule;
 val fold_tac     = meta Raw_Simplifier.fold_goals_tac;
 
+end;
+
 
 (* derived defs -- potentially within the object-logic *)
 
diff -r 0a8a75e400da -r 8b9401bfd9fd src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Apr 28 11:47:01 2016 +0200
+++ b/src/Pure/drule.ML	Thu Apr 28 15:42:52 2016 +0200
@@ -447,8 +447,7 @@
 local
 
 fun contract_lhs th =
-  Thm.transitive (Thm.symmetric (beta_eta_conversion
-    (fst (Thm.dest_equals (Thm.cprop_of th))))) th;
+  Thm.transitive (Thm.symmetric (beta_eta_conversion (#1 (Thm.dest_equals (Thm.cprop_of th))))) th;
 
 fun var_args ct =
   (case try Thm.dest_comb ct of