src/ZF/Inductive_ZF.thy

 
 setup IndCases.setup
 setup DatatypeTactics.setup
 
 ML_setup {*
-val iT = Ind_Syntax.iT
-and oT = FOLogic.oT;
-
 structure Lfp =
   struct
   val oper      = @{const lfp}
   val bnd_mono  = @{const bnd_mono}
   val bnd_monoI = @{thm bnd_monoI}