src/Tools/induct.ML

           induct x       - type induction
     ...   induct ... r   - explicit rule
 *)
 
 fun get_inductT ctxt insts =
-  fold_rev multiply (insts |> map
+  fold_rev (map_product cons) (insts |> map
       ((fn [] => NONE | ts => List.last ts) #>
         (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
         find_inductT ctxt)) [[]]
   |> filter_out (forall Thm.is_internal);