# HG changeset patch
# User wenzelm
# Date 1425682377 -3600
# Node ID 025f70f35daf7be12b2041f659a254947b79749d
# Parent  4b94cc030ba08804d70187313083549f32be6edc
clarified context;

diff -r 4b94cc030ba0 -r 025f70f35daf src/HOL/Nominal/nominal_datatype.ML
--- 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
diff -r 4b94cc030ba0 -r 025f70f35daf src/HOL/Nominal/nominal_fresh_fun.ML
--- 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
diff -r 4b94cc030ba0 -r 025f70f35daf src/HOL/Nominal/nominal_induct.ML
--- 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;