--- a/TFL/dcterm.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/TFL/dcterm.ML Wed Apr 04 23:29:33 2007 +0200
@@ -187,9 +187,9 @@
*---------------------------------------------------------------------------*)
fun mk_prop ctm =
- let val {t, sign, ...} = Thm.rep_cterm ctm in
+ let val {t, thy, ...} = Thm.rep_cterm ctm in
if can HOLogic.dest_Trueprop t then ctm
- else Thm.cterm_of sign (HOLogic.mk_Trueprop t)
+ else Thm.cterm_of thy (HOLogic.mk_Trueprop t)
end
handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
| TERM (msg, _) => raise ERR "mk_prop" msg;