1.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Jul 14 19:28:39 2005 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Jul 14 19:28:40 2005 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4   : INDUCTIVE_PACKAGE =
     1.5  struct
     1.6  
     1.7 -open Logic Ind_Syntax;
     1.8 +open Ind_Syntax;
     1.9  
    1.10  val co_prefix = if coind then "co" else "";
    1.11  
    1.12 @@ -112,7 +112,7 @@
    1.13  
    1.14    (*Makes a disjunct from an introduction rule*)
    1.15    fun fp_part intr = (*quantify over rule's free vars except parameters*)
    1.16 -    let val prems = map dest_tprop (strip_imp_prems intr)
    1.17 +    let val prems = map dest_tprop (Logic.strip_imp_prems intr)
    1.18          val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
    1.19          val exfrees = term_frees intr \\ rec_params
    1.20          val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
    1.21 @@ -138,7 +138,7 @@
    1.22  
    1.23    val fp_rhs = Fp.oper $ dom_sum $ fp_abs
    1.24  
    1.25 -  val dummy = List.app (fn rec_hd => deny (rec_hd occs fp_rhs)
    1.26 +  val dummy = List.app (fn rec_hd => deny (Logic.occs (rec_hd, fp_rhs))
    1.27                               "Illegal occurrence of recursion operator")
    1.28             rec_hds;
    1.29