src/HOL/Tools/primrec.ML

--- a/src/HOL/Tools/primrec.ML	Fri Oct 01 14:27:51 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Fri Oct 01 14:47:46 2010 +0200
@@ -78,7 +78,7 @@
     else
      (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
       check_vars "extra variables on rhs: "
-        (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
+        (Term.add_frees rhs [] |> subtract (op =) lfrees
           |> filter_out (is_fixed o fst));
       (case AList.lookup (op =) rec_fns fname of
         NONE =>