--- a/Nominal/nominal_function_core.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Mar 22 12:18:30 2016 +0000
@@ -22,7 +22,7 @@
         * thm list (* GIntros *)
         * thm (* Ginduct *) 
         * thm  (* goalstate *)
-        * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
+        * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
        ) * local_theory
 
   val inductive_def : (binding * typ) * mixfix -> term list -> local_theory 
@@ -520,7 +520,7 @@
     val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
 
     val exactly_one =
-      ex1I |> instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
+      ex1I |> Thm.instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
       |> curry (op COMP) existence
       |> curry (op COMP) uniqueness
       |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
@@ -556,7 +556,7 @@
     val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
-      |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
+      |> Thm.instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
     val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
     val ih_inv =  ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop}))
 
@@ -602,6 +602,7 @@
   let 
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
       lthy
+      |> Config.put Inductive.inductive_internals true
       |> Proof_Context.concealed
       |> Inductive.add_inductive_i
           {quiet_mode = true,
@@ -616,6 +617,7 @@
           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
           [] (* no special monos *)
       ||> Proof_Context.restore_naming lthy
+      ||> Config.put Inductive.inductive_internals (Config.get lthy Inductive.inductive_internals)
 
     val cert = Thm.cterm_of lthy
     fun requantify orig_intro thm =
@@ -849,9 +851,9 @@
       subset_induct_rule
       |> Thm.forall_intr (Thm.cterm_of ctxt D)
       |> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
-      |> atac 1 |> Seq.hd
+      |> assume_tac ctxt 1 |> Seq.hd
       |> (curry op COMP) (acc_downward
-        |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)]
+        |> (Thm.instantiate' [SOME (Thm.ctyp_of ctxt domT)]
              (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
         |> Thm.forall_intr (Thm.cterm_of ctxt z)
         |> Thm.forall_intr (Thm.cterm_of ctxt x))
@@ -1063,11 +1065,8 @@
       (prove_stuff lthy globals G f R xclauses complete compat
          compat_store G_elim G_eqvt invariant) f_defthm
      
-    fun mk_partial_rules provedgoal =
+    fun mk_partial_rules newctxt provedgoal =
       let
-        val newthy = Thm.theory_of_thm provedgoal (*FIXME*)
-        val newctxt = Proof_Context.init_global newthy (*FIXME*)
-
         val ((graph_is_function, complete_thm), graph_is_eqvt) =
           provedgoal
           |> Conjunction.elim