diff -r 66923825628e -r 66e1f24d655d src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Jul 23 16:45:04 2007 +0200
+++ b/src/Pure/Isar/method.ML	Mon Jul 23 19:45:44 2007 +0200
@@ -69,7 +69,6 @@
   val done_text: text
   val sorry_text: bool -> text
   val finish_text: text option * bool -> Position.T -> text
-  exception METHOD_FAIL of (string * Position.T) * exn
   val method: theory -> src -> Proof.context -> method
   val method_i: theory -> src -> Proof.context -> method
   val add_methods: (bstring * (src -> Proof.context -> method) * string) list
@@ -406,8 +405,6 @@
 
 (* get methods *)
 
-exception METHOD_FAIL of (string * Position.T) * exn;
-
 fun method_i thy =
   let
     val meths = #2 (MethodsData.get thy);
@@ -415,7 +412,7 @@
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup meths name of
           NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
-        | SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src))
+        | SOME ((mth, _), _) => mth src)
       end;
   in meth end;