--- 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));
--- 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 *)
--- 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
--- 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 *)
--- 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