more precise treatment of theory vs. Proof.context;

--- a/src/HOL/Tools/Function/partial_function.ML	Mon May 20 17:11:17 2013 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon May 20 17:14:39 2013 +0200
@@ -255,11 +255,11 @@
     val unfold =
       (cterm_instantiate' (map (SOME o cert) [uncurry, F, curry]) fixp_eq
         OF [mono_thm, f_def])
-      |> Tactic.rule_by_tactic lthy (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy) 1);
+      |> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1);
 
     val mk_raw_induct =
       mk_curried_induct args args_ctxt (cert curry) (cert uncurry)
-      #> singleton (Variable.export args_ctxt lthy)
+      #> singleton (Variable.export args_ctxt lthy')
       #> (fn thm => cterm_instantiate' [SOME (cert F)] thm OF [mono_thm, f_def])
       #> Drule.rename_bvars' (map SOME (fname :: argnames @ argnames))
 

--- a/src/Pure/tactic.ML	Mon May 20 17:11:17 2013 +0200
+++ b/src/Pure/tactic.ML	Mon May 20 17:14:39 2013 +0200
@@ -85,8 +85,9 @@
 (*Makes a rule by applying a tactic to an existing rule*)
 fun rule_by_tactic ctxt tac rl =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val ctxt' = Variable.declare_thm rl ctxt;
-    val ((_, [st]), ctxt'') = Variable.import true [rl] ctxt';
+    val ((_, [st]), ctxt'') = Variable.import true [Thm.transfer thy rl] ctxt';
   in
     (case Seq.pull (tac st) of
       NONE => raise THM ("rule_by_tactic", 0, [rl])

--- a/src/ZF/Tools/inductive_package.ML	Mon May 20 17:11:17 2013 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Mon May 20 17:14:39 2013 +0200
@@ -252,15 +252,15 @@
   val dummy = writeln "  Proving the elimination rule...";
 
   (*Breaks down logical connectives in the monotonic function*)
-  val basic_elim_tac =
+  fun basic_elim_tac ctxt =
       REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
-                ORELSE' bound_hyp_subst_tac ctxt1))
+                ORELSE' bound_hyp_subst_tac ctxt))
       THEN prune_params_tac
           (*Mutual recursion: collapse references to Part(D,h)*)
       THEN (PRIMITIVE (fold_rule part_rec_defs));
 
   (*Elimination*)
-  val elim = rule_by_tactic (Proof_Context.init_global thy1) basic_elim_tac
+  val elim = rule_by_tactic (Proof_Context.init_global thy1) (basic_elim_tac ctxt1)
                  (unfold RS Ind_Syntax.equals_CollectD)
 
   (*Applies freeness of the given constructors, which *must* be unfolded by
@@ -269,7 +269,7 @@
     Proposition A should have the form t:Si where Si is an inductive set*)
   fun make_cases ctxt A =
     rule_by_tactic ctxt
-      (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac)
+      (basic_elim_tac ctxt THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac ctxt)
       (Thm.assume A RS elim)
       |> Drule.export_without_context_open;