1.1 --- a/src/HOL/Set.thy	Tue Feb 14 16:59:12 2012 +0100
     1.2 +++ b/src/HOL/Set.thy	Tue Feb 14 17:11:33 2012 +0100
     1.3 @@ -379,7 +379,7 @@
     1.4  *}
     1.5  
     1.6  declaration {* fn _ =>
     1.7 -  Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
     1.8 +  Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
     1.9  *}
    1.10  
    1.11  ML {*