diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -69,7 +69,7 @@
     else
      (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
       check_vars "extra variables on rhs: "
-        (map dest_Free (term_frees rhs) |> subtract (op =) lfrees
+        (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
           |> filter_out (is_fixed o fst));
       case AList.lookup (op =) rec_fns fname of
         NONE =>