# HG changeset patch
# User wenzelm
# Date 910622338 -3600
# Node ID 5b79fbf1a65f8a1627498d0cb8e47742b2d7e04d
# Parent  c6fea8488ce7101386f0f8b51dbf265975e17aaa
added lift_modifier, rule;

diff -r c6fea8488ce7 -r 5b79fbf1a65f src/Pure/attribute.ML
--- a/src/Pure/attribute.ML	Mon Nov 09 15:36:27 1998 +0100
+++ b/src/Pure/attribute.ML	Mon Nov 09 15:38:58 1998 +0100
@@ -17,6 +17,8 @@
   include BASIC_ATTRIBUTE
   val thm_of: tthm -> thm
   val tthm_of: thm -> tthm
+  val lift_modifier: ('a * thm list -> 'b) -> 'a * tthm list -> 'b
+  val rule: ('b -> 'a) -> ('a -> thm -> thm) -> 'b attribute
   val none: 'a -> 'a * 'b attribute list
   val no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list
   val no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list
@@ -47,6 +49,10 @@
 fun thm_of (thm, _) = thm;
 fun tthm_of thm = (thm, []);
 
+fun lift_modifier f (x, tthms) = f (x, map thm_of tthms);
+
+fun rule get_data f (x, (thm, tags)) = (x, (f (get_data x) thm, tags));
+
 fun none x = (x, []);
 fun no_attrs (x, y) = ((x, (y, [])), []);
 fun no_attrss (x, ys) = ((x, map (rpair []) ys), []);