diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Set.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -379,8 +379,8 @@
   Gives better instantiation for bound:
 *}
 
-declaration {* fn _ =>
-  Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
+setup {*
+  map_theory_claset (fn ctxt => ctxt addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
 *}
 
 ML {*