1.1 --- a/src/Pure/context.ML	Tue Jul 20 14:41:13 2010 +0200
     1.2 +++ b/src/Pure/context.ML	Tue Jul 20 14:44:33 2010 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4  fun invoke f k =
     1.5    (case Datatab.lookup (! kinds) k of
     1.6      SOME kind => f kind
     1.7 -  | NONE => sys_error "Invalid theory data identifier");
     1.8 +  | NONE => raise Fail "Invalid theory data identifier");
     1.9  
    1.10  in
    1.11  
    1.12 @@ -459,7 +459,7 @@
    1.13  fun invoke_init k =
    1.14    (case Datatab.lookup (! kinds) k of
    1.15      SOME init => init
    1.16 -  | NONE => sys_error "Invalid proof data identifier");
    1.17 +  | NONE => raise Fail "Invalid proof data identifier");
    1.18  
    1.19  fun init_data thy =
    1.20    Datatab.map' (fn k => fn _ => invoke_init k thy) (! kinds);