TFL/mask.sml
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
child 3302 404fe31fd8d2
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
paulson@2112
     1
(*---------------------------------------------------------------------------
paulson@2112
     2
 * This structure is intended to shield TFL from any constructors already 
paulson@2112
     3
 * declared in the environment. In the Isabelle port, for example, there
paulson@2112
     4
 * was already a datatype with "|->" being a constructor. In TFL we were
paulson@2112
     5
 * trying to define a function "|->", but it failed in PolyML (which conforms
paulson@2112
     6
 * better to the Standard) while the definition was accepted in NJ/SML
paulson@2112
     7
 * (which doesn't always conform so well to the standard).
paulson@2112
     8
 *---------------------------------------------------------------------------*)
paulson@2112
     9
paulson@2112
    10
structure Mask : Mask_sig =
paulson@2112
    11
struct
paulson@2112
    12
paulson@2112
    13
 datatype 'a binding = |-> of ('a * 'a)   (* infix 7 |->; *)
paulson@2112
    14
paulson@2112
    15
 datatype mask = ERR 
paulson@2112
    16
end;