src/ZF/Tools/inductive_package.ML

 functor Add_inductive_def_Fun
     (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU val coind: bool)
  : INDUCTIVE_PACKAGE =
 struct
 
-open Logic Ind_Syntax;
+open Ind_Syntax;
 
 val co_prefix = if coind then "co" else "";
 
 
 (* utils *)

     | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
                             Sign.string_of_term sign Q);
 
   (*Makes a disjunct from an introduction rule*)
   fun fp_part intr = (*quantify over rule's free vars except parameters*)
-    let val prems = map dest_tprop (strip_imp_prems intr)
+    let val prems = map dest_tprop (Logic.strip_imp_prems intr)
         val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
         val exfrees = term_frees intr \\ rec_params
         val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
     in foldr FOLogic.mk_exists
              (fold_bal FOLogic.mk_conj (zeq::prems)) exfrees

                    mk_Collect(z', dom_sum,
                               fold_bal FOLogic.mk_disj part_intrs));
 
   val fp_rhs = Fp.oper $ dom_sum $ fp_abs
 
-  val dummy = List.app (fn rec_hd => deny (rec_hd occs fp_rhs)
+  val dummy = List.app (fn rec_hd => deny (Logic.occs (rec_hd, fp_rhs))
                              "Illegal occurrence of recursion operator")
            rec_hds;
 
   (*** Make the new theory ***)