# HG changeset patch
# User wenzelm
# Date 1112858853 -7200
# Node ID 963cd3f7976c6a50f69bb03926c1edd1fce22b95
# Parent  2b1f1902505dd9a455b0bb2eba3d3f2c0b75efa8
invalidated former constructors None/OPTION to prevent accidental use as match-all patterns!

diff -r 2b1f1902505d -r 963cd3f7976c src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Apr 07 09:27:20 2005 +0200
+++ b/src/Pure/library.ML	Thu Apr 07 09:27:33 2005 +0200
@@ -37,6 +37,11 @@
 
   (*options*)
   val is_none: 'a option -> bool
+
+  (*old options -- invalidated*)
+  datatype invalid = None of invalid
+  exception OPTION of invalid
+
   exception ERROR
   val try: ('a -> 'b) -> 'a -> 'b option
   val can: ('a -> 'b) -> 'a -> bool
@@ -317,15 +322,14 @@
 (** options **)
 
 val the = valOf;
-
-(*strict!*)
-fun if_none opt a = getOpt(opt,a);
-
+fun if_none opt a = getOpt (opt, a);
 val is_some = isSome;
+fun is_none opt = not (isSome opt);
+val apsome = Option.map;
 
-fun is_none opt = not (isSome opt);
-
-val apsome = Option.map;
+(*invalidate former constructors to prevent accidental use as match-all patterns!*)
+datatype invalid = None of invalid;
+exception OPTION of invalid;
 
 
 (* exception handling *)
@@ -586,9 +590,7 @@
 
 (*copy the list preserving elements that satisfy the predicate*)
 val filter = List.filter;
-
 fun filter_out f = filter (not o f);
-
 val mapfilter = List.mapPartial;