TFL/dcterm.sml
changeset 6397 e70ae9b575cc
parent 3405 2cccd0e3e9ea
child 7225 0a7c43c56092
--- a/TFL/dcterm.sml	Wed Mar 17 17:19:18 1999 +0100
+++ b/TFL/dcterm.sml	Wed Mar 17 17:20:36 1999 +0100
@@ -61,7 +61,7 @@
  *---------------------------------------------------------------------------*)
 
 fun mk_const sign pr = cterm_of sign (Const pr);
-val mk_hol_const = mk_const (sign_of HOL.thy);
+val mk_hol_const = mk_const (Theory.sign_of HOL.thy);
 
 fun mk_exists (r as (Bvar,Body)) = 
   let val ty = #T(rep_cterm Bvar)
@@ -181,7 +181,7 @@
 (*---------------------------------------------------------------------------
  * Going into and out of prop
  *---------------------------------------------------------------------------*)
-local val prop = cterm_of (sign_of HOL.thy) (read"Trueprop")
+local val prop = cterm_of (Theory.sign_of HOL.thy) (read"Trueprop")
 in fun mk_prop ctm =
      case (#t(rep_cterm ctm))
        of (Const("Trueprop",_)$_) => ctm