
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 {*




