theory Barf
imports Main Category
begin

  locale foo =
    fixes X
    assumes "X = X"

  context foo
  begin

    datatype (discs_sels) 't "term" =
      C
    | T "'t term * 't term"

end