diff -r b074c05f00ad -r e02b3a32f34f src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Jan 02 16:21:47 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Jan 02 22:06:56 2009 +0100
@@ -63,9 +63,10 @@
 
 fun inst_case_thm thy x P thm =
     let
-        val [Pv, xv] = OldTerm.term_vars (prop_of thm)
+        val [Pv, xv] = Term.add_vars (prop_of thm) []
     in
-        cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
+        cterm_instantiate [(cterm_of thy (Var xv), cterm_of thy x), 
+                           (cterm_of thy (Var Pv), cterm_of thy P)] thm
     end