diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/function_package/fundef_datatype.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
 A package for general recursive function definitions.
@@ -64,7 +63,7 @@
 
 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