# [isabelle] Exception Chr raised while processing "fun" (Isabelle 2016)

```Any ideas about the following?

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 â 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

```
```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
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.