src/HOL/Tools/function_package/fundef_datatype.ML

 (*  Title:      HOL/Tools/function_package/fundef_datatype.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
 A package for general recursive function definitions.
 A tactic to prove completeness of datatype patterns.
 *)

     forall_elim inst (forall_intr var thm)
 
 
 fun inst_case_thm thy x P thm =
     let
-        val [Pv, xv] = term_vars (prop_of thm)
+        val [Pv, xv] = OldTerm.term_vars (prop_of thm)
     in
         cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
     end