187 text {*

   187 text {*

   188   While the generic proof is relatively simple, it is a bit harder to

   188   While the generic proof is relatively simple, it is a bit harder to

   189   set up the goals for the induction principles. 

   189   set up the goals for the induction principles. 

   190 *}

   190 *}

   191 

   191 

   192 

   194 

   193 ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =

   195 ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =

   194 let

   196 let

   195   val Ps = replicate (length preds) "P"

   197   val Ps = replicate (length preds) "P"

   196   val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1

   198   val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1