src/HOL/Datatype.thy
changeset 17876 b9c92f384109
parent 17458 e42bfad176eb
child 18230 4dc1f30af6a1
--- a/src/HOL/Datatype.thy	Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Datatype.thy	Mon Oct 17 23:10:13 2005 +0200
@@ -169,7 +169,7 @@
 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   by simp
 
-ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *}
+ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
 
 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   by (cases xo) auto