src/Pure/Isar/method.ML
changeset 23937 66e1f24d655d
parent 23922 707639e9497d
child 24010 2ef318813e1a
     1.1 --- a/src/Pure/Isar/method.ML	Mon Jul 23 16:45:04 2007 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Jul 23 19:45:44 2007 +0200
     1.3 @@ -69,7 +69,6 @@
     1.4    val done_text: text
     1.5    val sorry_text: bool -> text
     1.6    val finish_text: text option * bool -> Position.T -> text
     1.7 -  exception METHOD_FAIL of (string * Position.T) * exn
     1.8    val method: theory -> src -> Proof.context -> method
     1.9    val method_i: theory -> src -> Proof.context -> method
    1.10    val add_methods: (bstring * (src -> Proof.context -> method) * string) list
    1.11 @@ -406,8 +405,6 @@
    1.12  
    1.13  (* get methods *)
    1.14  
    1.15 -exception METHOD_FAIL of (string * Position.T) * exn;
    1.16 -
    1.17  fun method_i thy =
    1.18    let
    1.19      val meths = #2 (MethodsData.get thy);
    1.20 @@ -415,7 +412,7 @@
    1.21        let val ((name, _), pos) = Args.dest_src src in
    1.22          (case Symtab.lookup meths name of
    1.23            NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
    1.24 -        | SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src))
    1.25 +        | SOME ((mth, _), _) => mth src)
    1.26        end;
    1.27    in meth end;
    1.28