src/HOL/Set.thy
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 {*