theory Barf
imports Main
begin

    datatype 't "term" =
      Const 't
    | U
    | T "'t term * 't term"
    | C "'t term * 't term"
    | L "'t term"
    | L' "'t term"
    | R "'t term"
    | R' "'t term"
    | A "'t term * 't term * 't term"
    | A' "'t term * 't term * 't term"

    fun F :: "'a term \<Rightarrow> int"
    where "F (T (T (U, b), c)) = 1 + F (T (U, T (b, c)))"
        | "F (T (T (a, b), c)) = 1 + F a + F (T (b, c))"
        | "F (T (U, b)) = 1 + F b"
        | "F (T (a, U)) = 1 + F a"
        | "F (T (a, b)) = (F a) + (F b)"
        | "F a = undefined"

    (* exception Chr raised (line 268 of "./basis/String.sml") *)
end