# HG changeset patch
# User wenzelm
# Date 1464372786 -7200
# Node ID d36c7dc40000e7711f91f9f3e01eb099eb3f3ed6
# Parent  466177e5736c067f8b9c696ca6462fc3ffa836ea
clarified "unfold" operations;

diff -r 466177e5736c -r d36c7dc40000 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Fri May 27 12:53:14 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML	Fri May 27 20:13:06 2016 +0200
@@ -29,6 +29,9 @@
   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
+  val unfold0: Proof.context -> thm list -> thm -> thm
+  val unfold0_goals: Proof.context -> thm list -> thm -> thm
+  val unfold0_tac: Proof.context -> thm list -> tactic
   val fold: Proof.context -> thm list -> thm -> thm
   val fold_tac: Proof.context -> thm list -> tactic
   val derived_def: Proof.context -> {conditional: bool} -> term ->
@@ -202,27 +205,40 @@
 fun abs_def_rule ctxt = meta_rewrite_rule ctxt #> Drule.abs_def;
 
 
-(* rewriting with object-level rules *)
+(* unfold 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 gen_unfold rewrite ctxt rews =
+  let val meta_rews = map (meta_rewrite_rule ctxt) rews in
+    if Config.get ctxt unfold_abs_def then
+      rewrite ctxt meta_rews #>
+      rewrite ctxt (map (perhaps (try Drule.abs_def)) meta_rews)
+    else rewrite ctxt meta_rews
+  end;
 
-fun meta f ctxt = f ctxt o map (meta_rewrite_rule ctxt);
+val no_unfold_abs_def = Config.put unfold_abs_def false;
 
 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;
+val unfold = gen_unfold Raw_Simplifier.rewrite_rule;
+val unfold_goals = gen_unfold Raw_Simplifier.rewrite_goals_rule;
+val unfold_tac = PRIMITIVE oo unfold_goals;
+
+val unfold0 = unfold o no_unfold_abs_def;
+val unfold0_goals = unfold_goals o no_unfold_abs_def;
+val unfold0_tac = unfold_tac o no_unfold_abs_def;
 
-end;
+end
+
+
+(* fold object-level rules *)
+
+fun fold ctxt rews = Raw_Simplifier.fold_rule ctxt (map (meta_rewrite_rule ctxt) rews);
+fun fold_tac ctxt rews = Raw_Simplifier.fold_goals_tac ctxt (map (meta_rewrite_rule ctxt) rews);
 
 
 (* derived defs -- potentially within the object-logic *)