# HG changeset patch
# User wenzelm
# Date 1272663789 -7200
# Node ID 0cbcdfd9e527118c65c9fbfd1df156ae5e9e5699
# Parent  8a041e2d812273d90d916bb88673cd81ced154a5
slightly more standard induct_simp_add/del attributes;
provide explicit context for internal addsimps;

diff -r 8a041e2d8122 -r 0cbcdfd9e527 src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Apr 30 23:40:14 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Apr 30 23:43:09 2010 +0200
@@ -342,8 +342,8 @@
         ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
           [Classical.safe_elim NONE]),
         ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]),
-        ((Binding.empty, flat (distinct @ inject)), [Induct.add_simp_rule])]
-        @ named_rules @ unnamed_rules)
+        ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
+          named_rules @ unnamed_rules)
     |> snd
     |> add_case_tr' case_names
     |> register dt_infos
diff -r 8a041e2d8122 -r 0cbcdfd9e527 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Apr 30 23:40:14 2010 +0200
+++ b/src/Tools/induct.ML	Fri Apr 30 23:43:09 2010 +0200
@@ -46,7 +46,8 @@
   val coinduct_pred: string -> attribute
   val coinduct_del: attribute
   val map_simpset: (simpset -> simpset) -> Context.generic -> Context.generic
-  val add_simp_rule: attribute
+  val induct_simp_add: attribute
+  val induct_simp_del: attribute
   val no_simpN: string
   val casesN: string
   val inductN: string
@@ -320,8 +321,14 @@
 val coinduct_del = del_att map3;
 
 fun map_simpset f = InductData.map (map4 f);
-fun add_simp_rule (ctxt, thm) =
-  (map_simpset (fn ss => ss addsimps [thm]) ctxt, thm);
+
+fun induct_simp f =
+  Thm.declaration_attribute (fn thm => fn context =>
+      (map_simpset
+        (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context));
+
+val induct_simp_add = induct_simp (op addsimps);
+val induct_simp_del = induct_simp (op delsimps);
 
 end;
 
@@ -359,7 +366,7 @@
     "declaration of induction rule" #>
   Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
     "declaration of coinduction rule" #>
-  Attrib.setup @{binding induct_simp} (Scan.succeed add_simp_rule)
+  Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
     "declaration of rules for simplifying induction or cases rules";
 
 end;