src/Pure/context.ML

 val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
 
 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
 
 fun invoke_empty k = invoke (K o #empty) k ();
 val invoke_extend = invoke #extend;

 val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
 
 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);
 
 fun init_new_data data thy =