diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -183,7 +183,7 @@
                 REPEAT_DETERM_N j distinct_tac,
                 TRY (dresolve_tac inject 1),
                 REPEAT (eresolve_tac [conjE] 1), hyp_subst_tac ctxt 1,
-                REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac 1]),
+                REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac ctxt 1]),
                 TRY (hyp_subst_tac ctxt 1),
                 resolve_tac [refl] 1,
                 REPEAT_DETERM_N (n - j - 1) distinct_tac],