--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Mar 06 15:58:56 2015 +0100
@@ -211,7 +211,7 @@
val (n1, t1) = args2typ n (snd con)
val (n2, t2) = cons2typ n1 cons
in (n2, mk_ssumT (t1, t2)) end
- val ct = Thm.ctyp_of thy (snd (cons2typ 1 spec'))
+ val ct = Thm.global_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