# HG changeset patch
# User wenzelm
# Date 1007376449 -3600
# Node ID 08afd1003151dfe10f47d5c8ae8b5bfd949cc46d
# Parent  24d31d47af1aba893573d851681557cf31254890
HOLogic.read_cterm;

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);
 
 
 (*---------------------------------------------------------------------------