changeset 12341 | 08afd1003151 |
parent 11771 | b7b100a2de1d |
child 12488 | 83acab8042ad |
--- a/TFL/post.ML Mon Dec 03 11:46:13 2001 +0100 +++ b/TFL/post.ML Mon Dec 03 11:47:29 2001 +0100 @@ -37,7 +37,7 @@ (* misc *) -fun read_term thy = Sign.simple_read_term (Theory.sign_of thy) HOLogic.termT; +val read_term = Thm.term_of oo (HOLogic.read_cterm o Theory.sign_of); (*---------------------------------------------------------------------------