src/HOL/HOLCF/Tools/Domain/domain_constructors.ML

     | arglist t = ([], t)
 in
   fun beta_of_def thy def_thm =
       let
         val (con, lam) =
-          Logic.dest_equals (Logic.unvarify_global (concl_of def_thm))
+          Logic.dest_equals (Logic.unvarify_global (Thm.concl_of def_thm))
         val (args, rhs) = arglist lam
         val lhs = list_ccomb (con, args)
         val goal = mk_equals (lhs, rhs)
         val cs = ContProc.cont_thms lam
         val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs

         | cons2typ n (con::cons) =
           let
             val (n1, t1) = args2typ n (snd con)
             val (n2, t2) = cons2typ n1 cons
           in (n2, mk_ssumT (t1, t2)) end
-      val ct = ctyp_of thy (snd (cons2typ 1 spec'))
+      val ct = Thm.ctyp_of thy (snd (cons2typ 1 spec'))
       val thm1 = instantiate' [SOME ct] [] @{thm exh_start}
       val thm2 = rewrite_rule (Proof_Context.init_global thy)
         (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
       val thm3 = rewrite_rule (Proof_Context.init_global thy)
         [mk_meta_eq @{thm conj_assoc}] thm2