# HG changeset patch
# User wenzelm
# Date 1285937266 -7200
# Node ID 63a1eb22d7d3c3a9ffb4fe9b0ca9eec6e4fb2d60
# Parent  d466bd29c887aeba84680df0caa99b528ea5bb3e
eliminated ancient OldTerm.term_frees;

diff -r d466bd29c887 -r 63a1eb22d7d3 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 =>