--- a/src/HOL/Nominal/nominal_datatype.ML Fri Mar 06 23:52:35 2015 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Mar 06 23:52:57 2015 +0100
@@ -108,9 +108,9 @@
val cp = cp_inst_of thy a b;
val dj = dj_thm_of thy b a;
val dj_cp' = [cp, dj] MRS dj_cp;
- val cert = SOME o Thm.global_cterm_of thy
+ val cert = SOME o Thm.cterm_of ctxt
in
- SOME (mk_meta_eq (Drule.instantiate' [SOME (Thm.global_ctyp_of thy S)]
+ SOME (mk_meta_eq (Drule.instantiate' [SOME (Thm.ctyp_of ctxt S)]
[cert t, cert r, cert s] dj_cp'))
end
else NONE