src/Pure/context.ML

--- a/src/Pure/context.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/context.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -120,7 +120,7 @@
 fun invoke f k =
   (case Datatab.lookup (! kinds) k of
     SOME kind => f kind
-  | NONE => sys_error "Invalid theory data identifier");
+  | NONE => raise Fail "Invalid theory data identifier");
 
 in
 
@@ -459,7 +459,7 @@
 fun invoke_init k =
   (case Datatab.lookup (! kinds) k of
     SOME init => init
-  | NONE => sys_error "Invalid proof data identifier");
+  | NONE => raise Fail "Invalid proof data identifier");
 
 fun init_data thy =
   Datatab.map' (fn k => fn _ => invoke_init k thy) (! kinds);