# HG changeset patch
# User huffman
# Date 1240409541 25200
# Node ID ac7e90792089c4a9dcdeda1048e32924c82a6c20
# Parent  96d053e00ec013fbd55484ec8a65730d6376738f
declare take_rews as simp rules

diff -r 96d053e00ec0 -r ac7e90792089 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Apr 21 17:07:44 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Apr 22 07:12:21 2009 -0700
@@ -608,23 +608,22 @@
 in
   thy
     |> Sign.add_path (Long_Name.base_name dname)
-    |> (snd o PureThy.add_thmss [
-        ((Binding.name "iso_rews" , iso_rews  ), [Simplifier.simp_add]),
-        ((Binding.name "exhaust"  , [exhaust] ), []),
-        ((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 "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]),
-        ((Binding.name "dist_les", dist_les), [Simplifier.simp_add]),
-        ((Binding.name "dist_eqs", dist_eqs), [Simplifier.simp_add]),
-        ((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])
-       ])
+    |> snd o PureThy.add_thmss [
+        ((Binding.name "iso_rews"  , iso_rews    ), [Simplifier.simp_add]),
+        ((Binding.name "exhaust"   , [exhaust]   ), []),
+        ((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 "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]),
+        ((Binding.name "dist_les"  , dist_les    ), [Simplifier.simp_add]),
+        ((Binding.name "dist_eqs"  , dist_eqs    ), [Simplifier.simp_add]),
+        ((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])]
     |> Sign.parent_path
     |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
         pat_rews @ dist_les @ dist_eqs @ copy_rews)
@@ -1004,14 +1003,14 @@
 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
 
 in thy |> Sign.add_path comp_dnam
-       |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
-		("take_rews"  , take_rews  ),
-		("take_lemmas", take_lemmas),
-		("finites"    , finites    ),
-		("finite_ind", [finite_ind]),
-		("ind"       , [ind       ]),
-		("coind"     , [coind     ])])))
-       |> (snd o (PureThy.add_thmss (map ind_rule (dnames ~~ inducts))))
+       |> snd o PureThy.add_thmss [
+           ((Binding.name "take_rews"  , take_rews   ), [Simplifier.simp_add]),
+           ((Binding.name "take_lemmas", take_lemmas ), []),
+           ((Binding.name "finites"    , finites     ), []),
+           ((Binding.name "finite_ind" , [finite_ind]), []),
+           ((Binding.name "ind"        , [ind]       ), []),
+           ((Binding.name "coind"      , [coind]     ), [])]
+       |> snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))
        |> Sign.parent_path |> pair take_rews
 end; (* let *)
 end; (* local *)