# HG changeset patch
# User wenzelm
# Date 911209470 -3600
# Node ID df19e1de5c8a6e4fc55c167bc5b5741de3e379a9
# Parent  2c037ffa728755490b37522464f8d0dd31416ef1
removed lift_modifier;
removed fail;
added tthms_of;
added print_tthm;
tuned rule;

diff -r 2c037ffa7287 -r df19e1de5c8a src/Pure/attribute.ML
--- a/src/Pure/attribute.ML	Mon Nov 16 10:42:40 1998 +0100
+++ b/src/Pure/attribute.ML	Mon Nov 16 10:44:30 1998 +0100
@@ -17,15 +17,16 @@
   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 thms_of: tthm list -> thm list
+  val tthms_of: thm list -> tthm list
+  val rule: ('a -> thm -> thm) -> 'a 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
-  val fail: string -> string -> 'a
   val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
   val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
   val pretty_tthm: tthm -> Pretty.T
+  val print_tthm: tthm -> unit
   val tag: tag -> 'a attribute
   val untag: tag -> 'a attribute
   val lemma: tag
@@ -49,9 +50,10 @@
 fun thm_of (thm, _) = thm;
 fun tthm_of thm = (thm, []);
 
-fun lift_modifier f (x, tthms) = f (x, map thm_of tthms);
+fun thms_of ths = map thm_of ths;
+fun tthms_of ths = map tthm_of ths;
 
-fun rule get_data f (x, (thm, tags)) = (x, (f (get_data x) thm, tags));
+fun rule f (x, (thm, _)) = (x, (f x thm, []));
 
 fun none x = (x, []);
 fun no_attrs (x, y) = ((x, (y, [])), []);
@@ -60,16 +62,8 @@
 
 (* apply attributes *)
 
-exception FAIL of string * string;
-
-fun fail name msg = raise FAIL (name, msg);
-
-(* FIXME error (!!?), push up the warning (??) *)
-fun warn_failed (name, msg) =
-  warning ("Failed invocation of " ^ quote name ^ " attribute: " ^ msg);
-
 fun apply (x_th, []) = x_th
-  | apply (x_th, f :: fs) = apply (f x_th handle FAIL info => (warn_failed info; x_th), fs);
+  | apply (x_th, f :: fs) = apply (f x_th, fs);
 
 fun applys ((x, []), _) = (x, [])
   | applys ((x, th :: ths), atts) =
@@ -88,6 +82,8 @@
   | pretty_tthm (thm, tags) = Pretty.block
       [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
 
+val print_tthm = Pretty.writeln o pretty_tthm;
+
 
 (* basic attributes *)