Conv.forall_conv: proper context;

--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 04 16:21:31 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 04 16:59:28 2007 +0200
@@ -26,8 +26,8 @@
   MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
     (HOL_basic_ss addsimps inductive_atomize);
 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
-val atomize_induct = Conv.fconv_rule (Conv.prems_conv ~1
-  (Conv.forall_conv ~1 (Conv.prems_conv ~1 atomize_conv)));
+fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
+  (Conv.forall_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
 
 val finite_Un = thm "finite_Un";
 val supp_prod = thm "supp_prod";
@@ -140,7 +140,7 @@
     val ctxt = ProofContext.init thy;
     val ({names, ...}, {raw_induct, ...}) =
       InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
-    val raw_induct = atomize_induct raw_induct;
+    val raw_induct = atomize_induct ctxt raw_induct;
     val monos = InductivePackage.get_monos ctxt;
     val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
     val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of
@@ -432,8 +432,8 @@
     val ctxt = ProofContext.init thy;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =
       InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
-    val raw_induct = atomize_induct raw_induct;
-    val elims = map atomize_induct elims;
+    val raw_induct = atomize_induct ctxt raw_induct;
+    val elims = map (atomize_induct ctxt) elims;
     val intrs = map atomize_intr intrs;
     val monos = InductivePackage.get_monos ctxt;
     val intrs' = InductivePackage.unpartition_rules intrs

--- a/src/Pure/Isar/object_logic.ML	Thu Oct 04 16:21:31 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML	Thu Oct 04 16:59:28 2007 +0200
@@ -160,7 +160,8 @@
 
 fun atomize_prems ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
-    Conv.forall_conv ~1 (Conv.prems_conv ~1 atomize) ct
+    Conv.forall_conv ~1 (K (Conv.prems_conv ~1 atomize))
+      (ProofContext.init (Thm.theory_of_cterm ct)) ct
   else Conv.all_conv ct;
 
 val atomize_prems_tac = CONVERSION atomize_prems;

--- a/src/Tools/induct.ML	Thu Oct 04 16:21:31 2007 +0200
+++ b/src/Tools/induct.ML	Thu Oct 04 16:59:28 2007 +0200
@@ -522,15 +522,15 @@
     | NONE => all_tac)
   end);
 
-fun miniscope_tac p =
-  CONVERSION (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
+fun miniscope_tac p = CONVERSION o
+  Conv.forall_conv p (K (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
 
 in
 
 fun fix_tac _ _ [] = K all_tac
   | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
      (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
-      (miniscope_tac (goal_params n goal))) i);
+      (miniscope_tac (goal_params n goal) ctxt)) i);
 
 end;