src/Pure/basis.ML
changeset 3047 599cb28f8502
parent 2884 4f2a4c27f9b5
child 3244 71b760618f30
equal deleted inserted replaced
3046:6b7935317538 3047:599cb28f8502
    31     | isSome NONE     = false
    31     | isSome NONE     = false
    32 
    32 
    33   fun valOf (SOME v) = v
    33   fun valOf (SOME v) = v
    34     | valOf NONE     = raise Option
    34     | valOf NONE     = raise Option
    35   end;
    35   end;
       
    36 
       
    37 open General;
    36 
    38 
    37 
    39 
    38 structure Int =
    40 structure Int =
    39   struct
    41   struct
    40   fun toString (i: int) = makestring i;
    42   fun toString (i: int) = makestring i;