Datatype diverges

The following session appears to diverge.

```
val it = ``:num``: hol_type
> val num = numSyntax.num;
val num = ``:num``: hol_type
> val _ = Datatype`num = Foo ^num | Bar`;
```

This one, however, converges quickly:

```
> val num = numSyntax.num;
val num = ``:num``: hol_type
> val _ = Hol_datatype`num = Foo of ^num | Bar`;
<<HOL message: Defined type: "num">>
```

Probably related to #257 
