--- 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
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Fri Mar 06 23:52:35 2015 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Fri Mar 06 23:52:57 2015 +0100
@@ -12,7 +12,6 @@
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
fun gen_res_inst_tac_term ctxt instf tyinst tinst elim th i st =
let
- val thy = Thm.theory_of_thm st;
val cgoal = nth (cprems_of st) (i - 1);
val maxidx = Thm.maxidx_of_cterm cgoal;
val j = maxidx + 1;
@@ -23,8 +22,8 @@
(head_of (Logic.incr_indexes (Ts, j) t),
fold_rev Term.abs ps u)) tinst;
val th' = instf
- (map (apply2 (Thm.global_ctyp_of thy)) tyinst')
- (map (apply2 (Thm.global_cterm_of thy)) tinst')
+ (map (apply2 (Thm.ctyp_of ctxt)) tyinst')
+ (map (apply2 (Thm.cterm_of ctxt)) tinst')
(Thm.lift_rule cgoal th)
in
compose_tac ctxt (elim, th', Thm.nprems_of th) i st
--- a/src/HOL/Nominal/nominal_induct.ML Fri Mar 06 23:52:35 2015 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Fri Mar 06 23:52:57 2015 +0100
@@ -83,9 +83,6 @@
fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
let
- val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.global_cterm_of thy;
-
val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm ctxt))) defs;