src/HOL/Tools/primrec_package.ML

     if length middle > 1 then
       primrec_error "more than one non-variable in pattern"
     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 =>
           (fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eqn))]))::rec_fns
       | SOME (_, rpos', eqns) =>