TFL/mask.sml
author paulson
Thu, 22 May 1997 15:13:16 +0200
changeset 3302 404fe31fd8d2
parent 2112 3902e9af752f
permissions -rw-r--r--
New headers and other minor changes

(*  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;