--- a/src/HOL/Tools/Function/induction_schema.ML Sat Nov 08 17:39:01 2014 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Sat Nov 08 21:31:51 2014 +0100
@@ -387,7 +387,7 @@
val nbranches = length branches
val npres = length pres
in
- Thm.bicompose {flatten = false, match = false, incremented = false}
+ Thm.bicompose (SOME ctxt') {flatten = false, match = false, incremented = false}
(false, res, length newgoals) i
THEN term_tac (i + nbranches + npres)
THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))