src/HOL/Option.ML
changeset 11655 923e4d0d36d5
parent 9343 1c4754938980
--- a/src/HOL/Option.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Option.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -78,7 +78,7 @@
 claset_ref() := claset() addSD2 ("ospec", ospec);
 
 
-Goal "x : o2s xo = (xo = Some x)";
+Goal "(x : o2s xo) = (xo = Some x)";
 by (case_tac "xo" 1);
 by Auto_tac;
 qed "elem_o2s";