src/HOL/Option.thy
changeset 39159 0dec18004e75
parent 39150 c4ff5fd8db99
child 39272 0b61951d2682
     1.1 --- a/src/HOL/Option.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/Option.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4    by simp
     1.5  
     1.6  declaration {* fn _ =>
     1.7 -  Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
     1.8 +  Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec}))
     1.9  *}
    1.10  
    1.11  lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"