Fix Induct_on for mutually/nested recursive types

[mn200]

Example problem:

val _ = Hol_datatype `ptree = Leaf of 'ts | Node of 'nts => ptree list`
val ptsize_def = Define`
   (ptsize (Leaf t) = 1) /\
   (ptsize (Node nt ps) = ptsizel ps + 1) /\
   (ptsizel [] = 0) /\
   (ptsizel (p::ps) = ptsize p + ptsizel ps)
`
val ptsize_gt0 = prove(
   ``!t. 0 < ptsize t``,
   Induct_on `t` (* raises exception *)
);

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.