src/Tools/induct.ML
changeset 36602 0cbcdfd9e527
parent 35625 9c818cab0dd0
child 36960 01594f816e3a
     1.1 --- a/src/Tools/induct.ML	Fri Apr 30 23:40:14 2010 +0200
     1.2 +++ b/src/Tools/induct.ML	Fri Apr 30 23:43:09 2010 +0200
     1.3 @@ -46,7 +46,8 @@
     1.4    val coinduct_pred: string -> attribute
     1.5    val coinduct_del: attribute
     1.6    val map_simpset: (simpset -> simpset) -> Context.generic -> Context.generic
     1.7 -  val add_simp_rule: attribute
     1.8 +  val induct_simp_add: attribute
     1.9 +  val induct_simp_del: attribute
    1.10    val no_simpN: string
    1.11    val casesN: string
    1.12    val inductN: string
    1.13 @@ -320,8 +321,14 @@
    1.14  val coinduct_del = del_att map3;
    1.15  
    1.16  fun map_simpset f = InductData.map (map4 f);
    1.17 -fun add_simp_rule (ctxt, thm) =
    1.18 -  (map_simpset (fn ss => ss addsimps [thm]) ctxt, thm);
    1.19 +
    1.20 +fun induct_simp f =
    1.21 +  Thm.declaration_attribute (fn thm => fn context =>
    1.22 +      (map_simpset
    1.23 +        (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context));
    1.24 +
    1.25 +val induct_simp_add = induct_simp (op addsimps);
    1.26 +val induct_simp_del = induct_simp (op delsimps);
    1.27  
    1.28  end;
    1.29  
    1.30 @@ -359,7 +366,7 @@
    1.31      "declaration of induction rule" #>
    1.32    Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
    1.33      "declaration of coinduction rule" #>
    1.34 -  Attrib.setup @{binding induct_simp} (Scan.succeed add_simp_rule)
    1.35 +  Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
    1.36      "declaration of rules for simplifying induction or cases rules";
    1.37  
    1.38  end;