# HG changeset patch
# User wenzelm
# Date 1126642764 -7200
# Node ID 11f959f0fe6ca81b2a30816ba849d1f5a41504a8
# Parent  ab97ccef124abd93e44538389f46fd9a5138aab3
replaced DATA_FAIL by EXCEPTION;

diff -r ab97ccef124a -r 11f959f0fe6c src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Sep 13 22:19:23 2005 +0200
+++ b/src/Pure/context.ML	Tue Sep 13 22:19:24 2005 +0200
@@ -19,7 +19,6 @@
 signature CONTEXT =
 sig
   include BASIC_CONTEXT
-  exception DATA_FAIL of exn * string
   (*theory context*)
   val theory_name: theory -> string
   val parents_of: theory -> theory list
@@ -107,8 +106,6 @@
 
 (* data kinds and access methods *)
 
-exception DATA_FAIL of exn * string;
-
 local
 
 type kind =
@@ -123,7 +120,7 @@
 fun invoke meth_name meth_fn k =
   (case Inttab.curried_lookup (! kinds) k of
     SOME kind => meth_fn kind |> transform_failure (fn exn =>
-      DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
+      EXCEPTION (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
 
 in
@@ -527,7 +524,7 @@
 fun invoke meth_name meth_fn k =
   (case Inttab.curried_lookup (! kinds) k of
     SOME kind => meth_fn kind |> transform_failure (fn exn =>
-      DATA_FAIL (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
+      EXCEPTION (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
 
 fun invoke_name k = invoke "name" (K o #name) k ();