| changeset 613 | f9eb0f819642 |
| parent 579 | 08f465e23dc5 |
| child 654 | 65435e2c6512 |
--- a/src/Pure/section_utils.ML Wed Sep 14 16:05:39 1994 +0200 +++ b/src/Pure/section_utils.ML Wed Sep 14 16:11:19 1994 +0200 @@ -20,8 +20,6 @@ fun get_def thy s = get_axiom thy (s^"_def"); -fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a); - (*Read an assumption in the given theory*) fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));