| changeset 6390 | 5d58c100ca3f |
| parent 6039 | 01f67f5f8dd0 |
| child 7744 | f27d54c1ef39 |
--- a/src/Pure/section_utils.ML Wed Mar 17 16:32:38 1999 +0100 +++ b/src/Pure/section_utils.ML Wed Mar 17 16:33:00 1999 +0100 @@ -15,7 +15,7 @@ (*Read an assumption in the given theory*) -fun assume_read thy a = Thm.assume (read_cterm (sign_of thy) (a,propT)); +fun assume_read thy a = Thm.assume (read_cterm (Theory.sign_of thy) (a,propT)); (*Read a term from string "b", with expected type T*) fun readtm sign T b =