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