(* Polymorphic Contexts *)

functor Ctx () :> CTX =
struct

  datatype 'a ctx =
    Null
  | $ of 'a ctx * 'a

  infix $

  fun nth (G $ A, 1) = A
    | nth (G $ A, n) = nth (G, n-1)
    | nth (Null, n) = raise Subscript

  fun member (x, G) =
      let fun mbr (Null) = false
	    | mbr (G $ y) = (x = y) orelse mbr G
      in mbr G end

end;  (* functor Ctx *)