# Re: [isabelle] HOLogic.dest_string

```Dear Matthias,

```
Indeed Const ("List.list.Cons", _) is the right implementation and not Const ("Cons", _). If you use the interactive mode and interpret e.g. ML{* @{term "Cons"} *} in a theory higher than List.thy, you will see that the output is indeed the first and not the second representation above. To convince yourself, you can try to certify a term built by just "Cons" e.g.
``` ML{* cterm_of @{theory} (Const("Cons",@{typ "'a list"}))*}
and you will see that Isabelle refuses this term as valid.

```
Terms (datatype term) as pointed out by Florian, is very liberal and contains many "ill-formed" terms.
```
Hope this helps,
Amine.

Matthias Berg wrote:
```
```Hi,

I just tried to use the function HOLogic.dest_string and it seems that
its pattern matching does not work. The function dest_list tries to
match terms like  (Const ("List.list.Cons", _) \$ t \$ u) but I think it
should be just (Const ("Cons", _) \$ t \$ u). The same problem occurs in
other functions as well. The following works for me:

fun dest_nibble t =
let fun err () = raise TERM ("dest_nibble", [t]) in
(case try (unprefix "Nibble" o fst o Term.dest_Const) t of
NONE => err ()
| SOME c =>
if size c <> 1 then err ()
else if "0" <= c andalso c <= "9" then ord c - ord "0"
else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
else err ())
end;
fun dest_char (Const ("Char", _) \$ t \$ u) =
dest_nibble t * 16 + dest_nibble u
| dest_char t = raise TERM ("dest_char", [t]);
fun dest_list (Const ("Nil", _)) = []
| dest_list (Const ("Cons", _) \$ t \$ u) = t :: dest_list u
| dest_list t = raise TERM ("dest_list", [t]);
val dest_string = implode o map (chr o dest_char) o dest_list;

Sincerely,
Matthias Berg

```
```

```

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