# HG changeset patch
# User wenzelm
# Date 1369494523 -7200
# Node ID 28963df2dffbe739becd32af57fe7e0eccc59939
# Parent  9065615d0360d77b159a1596e961bc445bd9f49e
tuned;

diff -r 9065615d0360 -r 28963df2dffb src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat May 25 16:55:27 2013 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sat May 25 17:08:43 2013 +0200
@@ -260,8 +260,8 @@
       THEN (PRIMITIVE (fold_rule part_rec_defs));
 
   (*Elimination*)
-  val elim = rule_by_tactic (Proof_Context.init_global thy1) (basic_elim_tac ctxt1)
-                 (unfold RS Ind_Syntax.equals_CollectD)
+  val elim =
+    rule_by_tactic ctxt1 (basic_elim_tac ctxt1) (unfold RS Ind_Syntax.equals_CollectD)
 
   (*Applies freeness of the given constructors, which *must* be unfolded by
       the given defs.  Cannot simply use the local con_defs because