TFL/dcterm.sml

 (*---------------------------------------------------------------------------
  * Some simple constructor functions.
  *---------------------------------------------------------------------------*)
 
 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)
       val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
   in capply c (uncurry cabs r)

 
 
 (*---------------------------------------------------------------------------
  * 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
         |  _ => capply prop ctm
 end;