diff -r 24d31d47af1a -r 08afd1003151 TFL/post.ML
--- 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);
 
 
 (*---------------------------------------------------------------------------