Provide print-only syntax for ground sptree values

E.g.,

> ``BN (LS v) (LS w)``;
<<HOL message: inventing new type variable names: 'a>>
val it = “⦕ 1 ↦ w; 2 ↦ v ⦖”: term

There's a trace to turn it off. Considering enabling it as input
syntax as well.