Fix <closetheory>

Replaced PolyML specific print function by Display.print_thm(s)

converted some induct_tac to induct

added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.

Replaced list of bound variables in simpset by maximal index of bound variables. This allows new variable names to be generated more quickly (without calling variant).

record_split_simp_tac now can get simp rules as parameter

update