src/HOL/Datatype.thy
changeset 26339 7825c83c9eff
parent 26146 61cb176d0385
child 26356 2312df2efa12
--- a/src/HOL/Datatype.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOL/Datatype.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -635,7 +635,9 @@
 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   by simp
 
-ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
+declaration {* fn _ =>
+  Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
+*}
 
 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   by (cases xo) auto