replaced DATA_FAIL by EXCEPTION;
authorwenzelm
Tue Sep 13 22:19:24 2005 +0200 (2005-09-13)
changeset 1734011f959f0fe6c
parent 17339 ab97ccef124a
child 17341 ca0e5105c4b1
replaced DATA_FAIL by EXCEPTION;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Tue Sep 13 22:19:23 2005 +0200
     1.2 +++ b/src/Pure/context.ML	Tue Sep 13 22:19:24 2005 +0200
     1.3 @@ -19,7 +19,6 @@
     1.4  signature CONTEXT =
     1.5  sig
     1.6    include BASIC_CONTEXT
     1.7 -  exception DATA_FAIL of exn * string
     1.8    (*theory context*)
     1.9    val theory_name: theory -> string
    1.10    val parents_of: theory -> theory list
    1.11 @@ -107,8 +106,6 @@
    1.12  
    1.13  (* data kinds and access methods *)
    1.14  
    1.15 -exception DATA_FAIL of exn * string;
    1.16 -
    1.17  local
    1.18  
    1.19  type kind =
    1.20 @@ -123,7 +120,7 @@
    1.21  fun invoke meth_name meth_fn k =
    1.22    (case Inttab.curried_lookup (! kinds) k of
    1.23      SOME kind => meth_fn kind |> transform_failure (fn exn =>
    1.24 -      DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
    1.25 +      EXCEPTION (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
    1.26    | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
    1.27  
    1.28  in
    1.29 @@ -527,7 +524,7 @@
    1.30  fun invoke meth_name meth_fn k =
    1.31    (case Inttab.curried_lookup (! kinds) k of
    1.32      SOME kind => meth_fn kind |> transform_failure (fn exn =>
    1.33 -      DATA_FAIL (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
    1.34 +      EXCEPTION (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
    1.35    | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
    1.36  
    1.37  fun invoke_name k = invoke "name" (K o #name) k ();