TFL/mask.sml
changeset 3353 9112a2efb9a3
parent 3352 04502e5431fb
child 3354 3dac85693547
--- a/TFL/mask.sml	Tue May 27 13:03:41 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(*  Title:      TFL/mask
-    ID:         $Id$
-    Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-*)
-
-(*---------------------------------------------------------------------------
- * This structure is intended to shield TFL from any constructors already 
- * declared in the environment. In the Isabelle port, for example, there
- * was already a datatype with "|->" being a constructor. In TFL we were
- * trying to define a function "|->", but it failed in PolyML (which conforms
- * better to the Standard) while the definition was accepted in NJ/SML
- * (which doesn't always conform so well to the standard).
- *---------------------------------------------------------------------------*)
-
-structure Mask : Mask_sig =
-struct
-
- datatype 'a binding = |-> of ('a * 'a)   (* infix 7 |->; *)
-
- datatype mask = ERR 
-end;