| changeset 58963 | 26bf09b95dda | 
| parent 58889 | 5b7a9633cfa8 | 
| child 59000 | 6eb0725503fc | 
--- 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 {*