# HG changeset patch
# User huffman
# Date 1257301950 28800
# Node ID 3182812d33ed2baf831bd665e4e7d5a7e2bd2442
# Parent  91df5fb651066fc8256220f48b990afd80a937b4
domain package registers fixrec_simp lemmas

diff -r 91df5fb65106 -r 3182812d33ed src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Nov 03 17:09:27 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Nov 03 18:32:30 2009 -0800
@@ -640,7 +640,8 @@
         ((Binding.name "casedist"  , [casedist]  ), [Induct.cases_type dname]),
         ((Binding.name "when_rews" , when_rews   ), [Simplifier.simp_add]),
         ((Binding.name "compacts"  , con_compacts), [Simplifier.simp_add]),
-        ((Binding.name "con_rews"  , con_rews    ), [Simplifier.simp_add]),
+        ((Binding.name "con_rews"  , con_rews    ),
+         [Simplifier.simp_add, Fixrec.fixrec_simp_add]),
         ((Binding.name "sel_rews"  , sel_rews    ), [Simplifier.simp_add]),
         ((Binding.name "dis_rews"  , dis_rews    ), [Simplifier.simp_add]),
         ((Binding.name "pat_rews"  , pat_rews    ), [Simplifier.simp_add]),
@@ -649,7 +650,8 @@
         ((Binding.name "inverts"   , inverts     ), [Simplifier.simp_add]),
         ((Binding.name "injects"   , injects     ), [Simplifier.simp_add]),
         ((Binding.name "copy_rews" , copy_rews   ), [Simplifier.simp_add]),
-        ((Binding.name "match_rews", mat_rews    ), [Simplifier.simp_add])]
+        ((Binding.name "match_rews", mat_rews    ),
+         [Simplifier.simp_add, Fixrec.fixrec_simp_add])]
     |> Sign.parent_path
     |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
         pat_rews @ dist_les @ dist_eqs @ copy_rews)
diff -r 91df5fb65106 -r 3182812d33ed src/HOLCF/Tools/fixrec.ML
--- 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))