# HG changeset patch
# User wenzelm
# Date 1417356710 -3600
# Node ID ec6ce25a630df2e895daca49c295f79fd7d875c4
# Parent  8606f2ee11b14109f6a10a1219987e38e377138b
more accurate context;

diff -r 8606f2ee11b1 -r ec6ce25a630d src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sun Nov 30 14:43:00 2014 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sun Nov 30 15:11:50 2014 +0100
@@ -230,7 +230,7 @@
      REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
                         ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
                                               type_elims)
-                        ORELSE' hyp_subst_tac ctxt1)),
+                        ORELSE' hyp_subst_tac ctxt)),
      if !Ind_Syntax.trace then print_tac ctxt "The subgoal after monos, type_elims:"
      else all_tac,
      DEPTH_SOLVE (swap_res_tac ctxt (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];