# HG changeset patch
# User wenzelm
# Date 1320672230 -3600
# Node ID dffa657f0aa21e1d03a42de5032f3360c3097fa3
# Parent  bf6add30ab20640e15f5a8353cf93cc7ddfd30e2
clarified attribute "mono_set": pure declaration, proper export in ML;

diff -r bf6add30ab20 -r dffa657f0aa2 NEWS
--- a/NEWS	Mon Nov 07 14:14:20 2011 +0100
+++ b/NEWS	Mon Nov 07 14:23:50 2011 +0100
@@ -19,6 +19,9 @@
 
 *** HOL ***
 
+* Clarified attribute "mono_set": pure declararation without modifying
+the result of the fact expression.
+
 * "Transitive_Closure.ntrancl": bounded transitive closure on
 relations.
 
diff -r bf6add30ab20 -r dffa657f0aa2 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon Nov 07 14:14:20 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Mon Nov 07 14:23:50 2011 +0100
@@ -22,6 +22,8 @@
     (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> Inductive.inductive_result * local_theory
+  val mono_add: attribute
+  val mono_del: attribute
   val codegen_preproc: theory -> thm list -> thm list
   val setup: theory -> theory
 end;
@@ -536,13 +538,12 @@
 val add_inductive_i = Inductive.gen_add_inductive_i add_ind_set_def;
 val add_inductive = Inductive.gen_add_inductive add_ind_set_def;
 
-fun mono_att att =  (* FIXME really mixed_attribute!? *)
-  Thm.mixed_attribute (fn (context, thm) =>
-    let val thm' = to_pred [] context thm
-    in (Thm.attribute_declaration att thm' context, thm') end);
+fun mono_att att =
+  Thm.declaration_attribute (fn thm => fn context =>
+    Thm.attribute_declaration att (to_pred [] context thm) context);
 
-val mono_add_att = mono_att Inductive.mono_add;
-val mono_del_att = mono_att Inductive.mono_del;
+val mono_add = mono_att Inductive.mono_add;
+val mono_del = mono_att Inductive.mono_del;
 
 
 (** package setup **)
@@ -556,7 +557,7 @@
     "convert rule to set notation" #>
   Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
     "convert rule to predicate notation" #>
-  Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
+  Attrib.setup @{binding mono_set} (Attrib.add_del mono_add mono_del)
     "declaration of monotonicity rule for set operators" #>
   Simplifier.map_simpset_global (fn ss => ss addsimprocs [collect_mem_simproc]);