changeset 4792 | 8e3c2dddb9c8 |
parent 4788 | b54c337f2c7f |
child 4853 | 67bcbb03c235 |
--- a/src/Pure/pure_thy.ML Sat Apr 04 11:44:16 1998 +0200 +++ b/src/Pure/pure_thy.ML Sat Apr 04 12:26:47 1998 +0200 @@ -86,7 +86,7 @@ fun get_theorems_sg sg = (case Sign.get_data sg theoremsK of Theorems r => r - | _ => sys_error "get_theorems_sg"); + | _ => type_error theoremsK); val get_theorems = get_theorems_sg o Theory.sign_of;