src/ZF/Tools/inductive_package.ML

--- a/src/ZF/Tools/inductive_package.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -193,9 +193,9 @@
         [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
          REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
 
-  val dom_subset = Drule.standard (big_rec_def RS Fp.subs);
+  val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
 
-  val unfold = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
+  val unfold = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.Tarski);
 
   (********)
   val dummy = writeln "  Proving the introduction rules...";
@@ -205,7 +205,7 @@
   val Part_trans =
       case rec_names of
            [_] => asm_rl
-         | _   => Drule.standard (@{thm Part_subset} RS @{thm subset_trans});
+         | _   => Drule.export_without_context (@{thm Part_subset} RS @{thm subset_trans});
 
   (*To type-check recursive occurrences of the inductive sets, possibly
     enclosed in some monotonic operator M.*)
@@ -272,7 +272,7 @@
     rule_by_tactic
       (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
       (Thm.assume A RS elim)
-      |> Drule.standard';
+      |> Drule.export_without_context_open;
 
   fun induction_rules raw_induct thy =
    let
@@ -503,7 +503,7 @@
      val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
 
      val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
-                  |> Drule.standard
+                  |> Drule.export_without_context
      and mutual_induct = CP.remove_split mutual_induct_fsplit
 
      val ([induct', mutual_induct'], thy') =
@@ -514,7 +514,7 @@
     in ((thy', induct'), mutual_induct')
     end;  (*of induction_rules*)
 
-  val raw_induct = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.induct)
+  val raw_induct = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.induct)
 
   val ((thy2, induct), mutual_induct) =
     if not coind then induction_rules raw_induct thy1