--- 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