src/HOLCF/Tools/fixrec.ML
changeset 33427 3182812d33ed
parent 33425 7e4f3c66190d
child 33430 c7dfeb7b0b0e
--- a/src/HOLCF/Tools/fixrec.ML	Tue Nov 03 17:09:27 2009 -0800
+++ b/src/HOLCF/Tools/fixrec.ML	Tue Nov 03 18:32:30 2009 -0800
@@ -13,8 +13,8 @@
   val add_fixpat: Thm.binding * term list -> theory -> theory
   val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
   val add_matchers: (string * string) list -> theory -> theory
-  val add_fixrec_simp: Thm.attribute
-  val del_fixrec_simp: Thm.attribute
+  val fixrec_simp_add: Thm.attribute
+  val fixrec_simp_del: Thm.attribute
   val fixrec_simp_tac: Proof.context -> int -> tactic
   val setup: theory -> theory
 end;
@@ -396,11 +396,11 @@
     SUBGOAL tac
   end;
 
-val add_fixrec_simp : Thm.attribute =
+val fixrec_simp_add : Thm.attribute =
   Thm.declaration_attribute
     (fn th => FixrecSimpData.map (fn ss => ss addsimps [th]));
 
-val del_fixrec_simp : Thm.attribute =
+val fixrec_simp_del : Thm.attribute =
   Thm.declaration_attribute
     (fn th => FixrecSimpData.map (fn ss => ss delsimps [th]));
 
@@ -527,7 +527,7 @@
 val setup =
   FixrecMatchData.init
   #> Attrib.setup @{binding fixrec_simp}
-                     (Attrib.add_del add_fixrec_simp del_fixrec_simp)
+                     (Attrib.add_del fixrec_simp_add fixrec_simp_del)
                      "declaration of fixrec simp rule"
   #> Method.setup @{binding fixrec_simp}
                      (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))