diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Set.thy --- a/src/HOL/Set.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Set.thy Mon Nov 10 21:49:48 2014 +0100 @@ -383,7 +383,7 @@ setup {* map_theory_claset (fn ctxt => - ctxt addbefore ("bspec", fn _ => dresolve_tac @{thms bspec} THEN' assume_tac)) + ctxt addbefore ("bspec", fn ctxt' => dresolve_tac @{thms bspec} THEN' assume_tac ctxt')) *} ML {*