Fix inftree

Fix inftreeScript, which defined its own case constant.

Fix was to get it to use Prim_rec.define_case_constant, which just
does the right thing.

This is progress with github issue #97.

Change export_rewrites back to its old API (without requiring an extra
string). When exported, the resulting simpset fragment always picked
up the name of the theory to be the base of its name, so there didn't
seem much point in giving users a false impression of naming power.

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

My pretty-printing wasn't pretty enough (caused an error, even) when using
the standard kernel.

Add a small theory of possibly infinitely branching trees. Leaf nodes
are labelled with 'a, internal nodes with 'b. The branching is modelled
as a function from 'c back into ('a,'b,'c)inftree. This is an algebraic
type with an initiality theorem, so it gets added to TypeBase. However,
bossLib.Induct doesn't work for values of this type (this is a bug I guess),
and I don't think primitive recursion will work either because of the way
the rhs of the iNd clause has the recursive function in a function
composition.
The clause is: f (iNd b cf) = nd b cf (f o cf)
This setup is sufficiently polymorphic that it could probably be used as
the basis for the definition of lots of other types (could get binary trees
by taking 'a to be unit, 'b to be 'a, and 'c to be bool). The theory
does depend on lists though.