src/ZF/Tools/inductive_package.ML

 (*  Title:      ZF/Tools/inductive_package.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
 
 Fixedpoint definition module -- for Inductive/Coinductive Definitions
 
 The functor will be instantiated for normal sums/products (inductive defs)
                          and non-standard sums/products (coinductive defs)

 
   (*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 (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 exfrees = OldTerm.term_frees intr \\ rec_params
         val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
     in foldr FOLogic.mk_exists
              (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees
     end;
 

                  in  subst_free (map mk_sb ind_alist) prem :: iprems  end)
        | add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
 
      (*Make a premise of the induction rule.*)
      fun induct_prem ind_alist intr =
-       let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
+       let val quantfrees = map dest_Free (OldTerm.term_frees intr \\ rec_params)
            val iprems = foldr (add_induct_prem ind_alist) []
                               (Logic.strip_imp_prems intr)
            val (t,X) = Ind_Syntax.rule_concl intr
            val (SOME pred) = AList.lookup (op aconv) ind_alist X
            val concl = FOLogic.mk_Trueprop (pred $ t)