diff -r 66923825628e -r 66e1f24d655d src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Jul 23 16:45:04 2007 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Jul 23 19:45:44 2007 +0200
@@ -14,7 +14,6 @@
 sig
   include BASIC_ATTRIB
   type src
-  exception ATTRIB_FAIL of (string * Position.T) * exn
   val intern: theory -> xstring -> string
   val intern_src: theory -> src -> src
   val pretty_attribs: Proof.context -> src list -> Pretty.T list
@@ -87,8 +86,6 @@
 
 (* get attributes *)
 
-exception ATTRIB_FAIL of (string * Position.T) * exn;
-
 fun attribute_i thy =
   let
     val attrs = #2 (AttributesData.get thy);
@@ -96,7 +93,7 @@
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup attrs name of
           NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
-        | SOME ((att, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (att src))
+        | SOME ((att, _), _) => att src)
       end;
   in attr end;