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

```Hi Eugene,

```
The problem seems to be with lexicographic_order (it probably tries to generate some error or info message in which a conversion to characters fails). If you use size_change in the termination proof, it works:
```
function (sequential) 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"
by pat_completeness auto
termination by size_change

Best,
Andreas

On 17/10/16 12:17, Eugene W. Stark wrote:
```
```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

```
```

```

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